Theorem trsbcVD 41218

Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc 40881 is trsbcVD 41218 without virtual deductions and was automatically derived from trsbcVD 41218.

1::	⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦)   )
3:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴)   )
4:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴)   )
5:1,2,3,4:	⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))   )
6:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)))   )
7:5,6:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))   )
8::	⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
9:7,8:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
10::	⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
11:10:	⊢ ∀𝑥((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
12:1,11:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ [𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))   )
13:9,12:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
14:13:	⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑦([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
15:14:	⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
16:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))   )
17:15,16:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
18:17:	⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑧([𝐴 / 𝑥]∀𝑦(( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
19:18:	⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑧[𝐴 / 𝑥]∀𝑦(( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
20:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑧∀𝑦(( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))   )
21:19,20:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑧∀𝑦(( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
22::	⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
23:21,22:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑧∀𝑦(( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ Tr 𝐴)   )
24::	⊢ (Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
25:24:	⊢ ∀𝑥(Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
26:1,25:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥 ↔ [𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))   )
27:23,26:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)   )
qed:27:	⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))

(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
trsbcVD	⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem trsbcVD

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 40915	. . . . . . . . . . . . . 14 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		sbcg 3849	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
3	1, 2	e1a 40968	. . . . . . . . . . . . . 14 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦)   )
4		sbcel2gv 3843	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴))
5	1, 4	e1a 40968	. . . . . . . . . . . . . 14 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴)   )
6		sbcel2gv 3843	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴))
7	1, 6	e1a 40968	. . . . . . . . . . . . . 14 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴)   )
8		imbi13 40861	. . . . . . . . . . . . . . 15 ⊢ (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦) → (([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴) → (([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴) → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))))))
9	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝐵 → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦) → (([𝐴 / 𝑥]𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴) → (([𝐴 / 𝑥]𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴) → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))))))
10	1, 3, 5, 7, 9	e1111 41016	. . . . . . . . . . . . 13 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))   )
11		sbcim2g 40879	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥))))
12	1, 11	e1a 40968	. . . . . . . . . . . . 13 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)))   )
13		bibi1 354	. . . . . . . . . . . . . 14 ⊢ (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥))) → (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) ↔ (([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))))
14	13	biimprcd 252	. . . . . . . . . . . . 13 ⊢ ((([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) → (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 → ([𝐴 / 𝑥]𝑦 ∈ 𝑥 → [𝐴 / 𝑥]𝑧 ∈ 𝑥))) → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))))
15	10, 12, 14	e11 41029	. . . . . . . . . . . 12 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))   )
16		pm3.31 452	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
17		pm3.3 451	. . . . . . . . . . . . 13 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴) → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)))
18	16, 17	impbii 211	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
19		bibi1 354	. . . . . . . . . . . . 13 ⊢ (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) → (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) ↔ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))))
20	19	biimprd 250	. . . . . . . . . . . 12 ⊢ (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴))) → (((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))))
21	15, 18, 20	e10 41035	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
22		pm3.31 452	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
23		pm3.3 451	. . . . . . . . . . . . . 14 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)))
24	22, 23	impbii 211	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
25	24	ax-gen 1796	. . . . . . . . . . . 12 ⊢ ∀𝑥((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
26		sbcbi 40880	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥((𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ [𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))))
27	1, 25, 26	e10 41035	. . . . . . . . . . 11 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ [𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))   )
28		bitr3 355	. . . . . . . . . . . 12 ⊢ (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ [𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → ([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))))
29	28	com12 32	. . . . . . . . . . 11 ⊢ (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (([𝐴 / 𝑥](𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑥)) ↔ [𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → ([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))))
30	21, 27, 29	e11 41029	. . . . . . . . . 10 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
31	30	gen11 40957	. . . . . . . . 9 ⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑦([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
32		albi 1819	. . . . . . . . 9 ⊢ (∀𝑦([𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
33	31, 32	e1a 40968	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
34		sbcal 3835	. . . . . . . . . 10 ⊢ ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
35	34	a1i 11	. . . . . . . . 9 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)))
36	1, 35	e1a 40968	. . . . . . . 8 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))   )
37		bibi1 354	. . . . . . . . 9 ⊢ (([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → (([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) ↔ (∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))))
38	37	biimprcd 252	. . . . . . . 8 ⊢ ((∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))))
39	33, 36, 38	e11 41029	. . . . . . 7 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
40	39	gen11 40957	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   ∀𝑧([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
41		albi 1819	. . . . . 6 ⊢ (∀𝑧([𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)))
42	40, 41	e1a 40968	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   (∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
43		sbcal 3835	. . . . . . 7 ⊢ ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
44	43	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)))
45	1, 44	e1a 40968	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))   )
46		bibi1 354	. . . . . 6 ⊢ (([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → (([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) ↔ (∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))))
47	46	biimprcd 252	. . . . 5 ⊢ ((∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → (([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧[𝐴 / 𝑥]∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))))
48	42, 45, 47	e11 41029	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))   )
49		dftr2 5176	. . . 4 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
50		biantr 804	. . . . 5 ⊢ ((([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) ∧ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))) → ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ Tr 𝐴))
51	50	ex 415	. . . 4 ⊢ (([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → ((Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)) → ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ Tr 𝐴)))
52	48, 49, 51	e10 41035	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ Tr 𝐴)   )
53		dftr2 5176	. . . . 5 ⊢ (Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
54	53	ax-gen 1796	. . . 4 ⊢ ∀𝑥(Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))
55		sbcbi 40880	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(Tr 𝑥 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → ([𝐴 / 𝑥]Tr 𝑥 ↔ [𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))))
56	1, 54, 55	e10 41035	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥 ↔ [𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥))   )
57		bibi1 354	. . . 4 ⊢ (([𝐴 / 𝑥]Tr 𝑥 ↔ [𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → (([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴) ↔ ([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ Tr 𝐴)))
58	57	biimprcd 252	. . 3 ⊢ (([𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ Tr 𝐴) → (([𝐴 / 𝑥]Tr 𝑥 ↔ [𝐴 / 𝑥]∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)))
59	52, 56, 58	e11 41029	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)   )
60	59	in1 40912	1 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   ∈ wcel 2114  [wsbc 3774  Tr wtr 5174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-sbc 3775  df-in 3945  df-ss 3954  df-uni 4841  df-tr 5175  df-vd1 40911

This theorem is referenced by: (None)