Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trsbcVD Structured version   Visualization version   GIF version

Theorem trsbcVD 41507
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 41170 is trsbcVD 41507 without virtual deductions and was automatically derived from trsbcVD 41507.
 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.
StepHypRef Expression
1 idn1 41204 . . . . . . . . . . . . . 14 (   𝐴𝐵   ▶   𝐴𝐵   )
2 sbcg 3831 . . . . . . . . . . . . . . 15 (𝐴𝐵 → ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦))
31, 2e1a 41257 . . . . . . . . . . . . . 14 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦)   )
4 sbcel2gv 3825 . . . . . . . . . . . . . . 15 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦𝑥𝑦𝐴))
51, 4e1a 41257 . . . . . . . . . . . . . 14 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝑥𝑦𝐴)   )
6 sbcel2gv 3825 . . . . . . . . . . . . . . 15 (𝐴𝐵 → ([𝐴 / 𝑥]𝑧𝑥𝑧𝐴))
71, 6e1a 41257 . . . . . . . . . . . . . 14 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑥𝑧𝐴)   )
8 imbi13 41150 . . . . . . . . . . . . . . 15 (([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) → (([𝐴 / 𝑥]𝑦𝑥𝑦𝐴) → (([𝐴 / 𝑥]𝑧𝑥𝑧𝐴) → (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))))))
98a1i 11 . . . . . . . . . . . . . 14 (𝐴𝐵 → (([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) → (([𝐴 / 𝑥]𝑦𝑥𝑦𝐴) → (([𝐴 / 𝑥]𝑧𝑥𝑧𝐴) → (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))))))
101, 3, 5, 7, 9e1111 41305 . . . . . . . . . . . . 13 (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))   )
11 sbcim2g 41168 . . . . . . . . . . . . . 14 (𝐴𝐵 → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥))))
121, 11e1a 41257 . . . . . . . . . . . . 13 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)))   )
13 bibi1 355 . . . . . . . . . . . . . 14 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥))) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))) ↔ (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))))
1413biimprcd 253 . . . . . . . . . . . . 13 ((([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥))) → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))))
1510, 12, 14e11 41318 . . . . . . . . . . . 12 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))   )
16 pm3.31 453 . . . . . . . . . . . . 13 ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
17 pm3.3 452 . . . . . . . . . . . . 13 (((𝑧𝑦𝑦𝐴) → 𝑧𝐴) → (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))
1816, 17impbii 212 . . . . . . . . . . . 12 ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
19 bibi1 355 . . . . . . . . . . . . 13 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) ↔ ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
2019biimprd 251 . . . . . . . . . . . 12 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))) → (((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
2115, 18, 20e10 41324 . . . . . . . . . . 11 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
22 pm3.31 453 . . . . . . . . . . . . . 14 ((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
23 pm3.3 452 . . . . . . . . . . . . . 14 (((𝑧𝑦𝑦𝑥) → 𝑧𝑥) → (𝑧𝑦 → (𝑦𝑥𝑧𝑥)))
2422, 23impbii 212 . . . . . . . . . . . . 13 ((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2524ax-gen 1797 . . . . . . . . . . . 12 𝑥((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
26 sbcbi 41169 . . . . . . . . . . . 12 (𝐴𝐵 → (∀𝑥((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))))
271, 25, 26e10 41324 . . . . . . . . . . 11 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
28 bitr3 356 . . . . . . . . . . . 12 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → ([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
2928com12 32 . . . . . . . . . . 11 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
3021, 27, 29e11 41318 . . . . . . . . . 10 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
3130gen11 41246 . . . . . . . . 9 (   𝐴𝐵   ▶   𝑦([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
32 albi 1820 . . . . . . . . 9 (∀𝑦([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
3331, 32e1a 41257 . . . . . . . 8 (   𝐴𝐵   ▶   (∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
34 sbcal 3818 . . . . . . . . . 10 ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
3534a1i 11 . . . . . . . . 9 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)))
361, 35e1a 41257 . . . . . . . 8 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
37 bibi1 355 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → (([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) ↔ (∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
3837biimprcd 253 . . . . . . . 8 ((∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
3933, 36, 38e11 41318 . . . . . . 7 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
4039gen11 41246 . . . . . 6 (   𝐴𝐵   ▶   𝑧([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
41 albi 1820 . . . . . 6 (∀𝑧([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
4240, 41e1a 41257 . . . . 5 (   𝐴𝐵   ▶   (∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
43 sbcal 3818 . . . . . . 7 ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
4443a1i 11 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)))
451, 44e1a 41257 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
46 bibi1 355 . . . . . 6 (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) ↔ (∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
4746biimprcd 253 . . . . 5 ((∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
4842, 45, 47e11 41318 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
49 dftr2 5160 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
50 biantr 805 . . . . 5 ((([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) ∧ (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))) → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴))
5150ex 416 . . . 4 (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → ((Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴)))
5248, 49, 51e10 41324 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴)   )
53 dftr2 5160 . . . . 5 (Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
5453ax-gen 1797 . . . 4 𝑥(Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
55 sbcbi 41169 . . . 4 (𝐴𝐵 → (∀𝑥(Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))))
561, 54, 55e10 41324 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
57 bibi1 355 . . . 4 (([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → (([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴) ↔ ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴)))
5857biimprcd 253 . . 3 (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴) → (([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)))
5952, 56, 58e11 41318 . 2 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)   )
6059in1 41201 1 (𝐴𝐵 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   ∈ wcel 2115  [wsbc 3758  Tr wtr 5158 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-sbc 3759  df-in 3926  df-ss 3936  df-uni 4825  df-tr 5159  df-vd1 41200 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator