Theorem psubsplitelof-P6 801

Description: Apply Proper Substitution to Split "Element Of" Predicate.

'𝑎' and '𝑏' are distinct form all other variables.

Assertion

Ref	Expression
psubsplitelof-P6	⊢ ([𝑤 / 𝑥] 𝑡 ∈ 𝑢 ↔ ∃𝑎∃𝑏(([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))

Distinct variable groups:   𝑡,𝑎   𝑢,𝑎   𝑤,𝑎   𝑡,𝑏   𝑢,𝑏   𝑤,𝑏,𝑎   𝑥,𝑎,𝑏

Proof of Theorem psubsplitelof-P6

Step	Hyp	Ref	Expression
1		splitelof-P6 778	. . 3 ⊢ (𝑡 ∈ 𝑢 ↔ ∃𝑎∃𝑏((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
2	1	psubleq-P6 783	. 2 ⊢ ([𝑤 / 𝑥] 𝑡 ∈ 𝑢 ↔ [𝑤 / 𝑥]∃𝑎∃𝑏((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
3		psubex2v-P6 797	. 2 ⊢ ([𝑤 / 𝑥]∃𝑎∃𝑏((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏) ↔ ∃𝑎[𝑤 / 𝑥]∃𝑏((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
4		psubex2v-P6 797	. . 3 ⊢ ([𝑤 / 𝑥]∃𝑏((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏) ↔ ∃𝑏[𝑤 / 𝑥]((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
5	4	subexinf-P5 608	. 2 ⊢ (∃𝑎[𝑤 / 𝑥]∃𝑏((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏) ↔ ∃𝑎∃𝑏[𝑤 / 𝑥]((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
6		psuband-P6 792	. . . . 5 ⊢ ([𝑤 / 𝑥]((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏) ↔ ([𝑤 / 𝑥](𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ [𝑤 / 𝑥] 𝑎 ∈ 𝑏))
7		psuband-P6 792	. . . . . 6 ⊢ ([𝑤 / 𝑥](𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ↔ ([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑏 = 𝑢))
8		psubnfr-P6.VR 785	. . . . . 6 ⊢ ([𝑤 / 𝑥] 𝑎 ∈ 𝑏 ↔ 𝑎 ∈ 𝑏)
9	7, 8	subandd-P3.42c.RC 344	. . . . 5 ⊢ (([𝑤 / 𝑥](𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ [𝑤 / 𝑥] 𝑎 ∈ 𝑏) ↔ (([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
10	6, 9	bitrns-P3.33c.RC 303	. . . 4 ⊢ ([𝑤 / 𝑥]((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏) ↔ (([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
11	10	subexinf-P5 608	. . 3 ⊢ (∃𝑏[𝑤 / 𝑥]((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏) ↔ ∃𝑏(([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
12	11	subexinf-P5 608	. 2 ⊢ (∃𝑎∃𝑏[𝑤 / 𝑥]((𝑎 = 𝑡 ∧ 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏) ↔ ∃𝑎∃𝑏(([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))
13	2, 3, 5, 12	tbitrns-P4.17.RC 431	1 ⊢ ([𝑤 / 𝑥] 𝑡 ∈ 𝑢 ↔ ∃𝑎∃𝑏(([𝑤 / 𝑥] 𝑎 = 𝑡 ∧ [𝑤 / 𝑥] 𝑏 = 𝑢) ∧ 𝑎 ∈ 𝑏))

Syntax hints:  term-obj 1   = wff-equals 6   ∈ wff-elemof 7   ↔ wff-bi 104   ∧ wff-and 132  ∃wff-exists 595  [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-L8-inl 20  ax-L8-inr 21  ax-L10 27  ax-L11 28  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: (None)