Theorem psubcomp-P6 767

Description: Composition of Proper Substitutions.

This can be taken as a definition of proper substitution for when '𝑥' occurs in '𝑡', given the definition where '𝑥' does not occur in '𝑡'.

'𝑦' cannot occur in either '𝜑' or '𝑡'.

Assertion

Ref	Expression
psubcomp-P6	⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑦][𝑦 / 𝑥]𝜑)

Distinct variable groups:   𝜑,𝑦   𝑡,𝑦   𝑥,𝑦

Proof of Theorem psubcomp-P6

Step	Hyp	Ref	Expression
1		lemma-L6.06a 766	. 2 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
2		lemma-L6.06a 766	. 2 ⊢ Ⅎ𝑦[𝑡 / 𝑦][𝑦 / 𝑥]𝜑
3		psubtoisub-P6 765	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
4		psubtoisub-P6 765	. 2 ⊢ (𝑦 = 𝑡 → ([𝑦 / 𝑥]𝜑 ↔ [𝑡 / 𝑦][𝑦 / 𝑥]𝜑))
5	1, 2, 3, 4	isubtopsub-P6 729	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ [𝑡 / 𝑦][𝑦 / 𝑥]𝜑)

Syntax hints:  term-obj 1   ↔ wff-bi 104  [wff-psub 714

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L10 27  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682  df-psub-D6.2 716

This theorem is referenced by:  psuball2v-P6  796  ndpsub4-P7.16  841