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

Theorem trsbcVD 39635
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 39275 is trsbcVD 39635 without virtual deductions and was automatically derived from trsbcVD 39635.
 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 39315 . . . . . . . . . . . . . 14 (   𝐴𝐵   ▶   𝐴𝐵   )
2 biidd 252 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 → (𝑧𝑦𝑧𝑦))
32sbcieg 3620 . . . . . . . . . . . . . . 15 (𝐴𝐵 → ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦))
41, 3e1a 39377 . . . . . . . . . . . . . 14 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦)   )
5 sbcel2gv 3647 . . . . . . . . . . . . . . 15 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦𝑥𝑦𝐴))
61, 5e1a 39377 . . . . . . . . . . . . . 14 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝑥𝑦𝐴)   )
7 sbcel2gv 3647 . . . . . . . . . . . . . . 15 (𝐴𝐵 → ([𝐴 / 𝑥]𝑧𝑥𝑧𝐴))
81, 7e1a 39377 . . . . . . . . . . . . . 14 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑥𝑧𝐴)   )
9 imbi13 39251 . . . . . . . . . . . . . . 15 (([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) → (([𝐴 / 𝑥]𝑦𝑥𝑦𝐴) → (([𝐴 / 𝑥]𝑧𝑥𝑧𝐴) → (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))))))
109a1i 11 . . . . . . . . . . . . . 14 (𝐴𝐵 → (([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) → (([𝐴 / 𝑥]𝑦𝑥𝑦𝐴) → (([𝐴 / 𝑥]𝑧𝑥𝑧𝐴) → (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))))))
111, 4, 6, 8, 10e1111 39425 . . . . . . . . . . . . 13 (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))   )
12 sbcim2g 39273 . . . . . . . . . . . . . 14 (𝐴𝐵 → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥))))
131, 12e1a 39377 . . . . . . . . . . . . 13 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)))   )
14 bibi1 340 . . . . . . . . . . . . . 14 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥))) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))) ↔ (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))))
1514biimprcd 240 . . . . . . . . . . . . 13 ((([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥))) → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))))
1611, 13, 15e11 39438 . . . . . . . . . . . 12 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))   )
17 pm3.31 436 . . . . . . . . . . . . 13 ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
18 pm3.3 435 . . . . . . . . . . . . 13 (((𝑧𝑦𝑦𝐴) → 𝑧𝐴) → (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))
1917, 18impbii 199 . . . . . . . . . . . 12 ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
20 bibi1 340 . . . . . . . . . . . . 13 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) ↔ ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
2120biimprd 238 . . . . . . . . . . . 12 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))) → (((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
2216, 19, 21e10 39444 . . . . . . . . . . 11 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
23 pm3.31 436 . . . . . . . . . . . . . 14 ((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
24 pm3.3 435 . . . . . . . . . . . . . 14 (((𝑧𝑦𝑦𝑥) → 𝑧𝑥) → (𝑧𝑦 → (𝑦𝑥𝑧𝑥)))
2523, 24impbii 199 . . . . . . . . . . . . 13 ((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2625ax-gen 1870 . . . . . . . . . . . 12 𝑥((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
27 sbcbi 39274 . . . . . . . . . . . 12 (𝐴𝐵 → (∀𝑥((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))))
281, 26, 27e10 39444 . . . . . . . . . . 11 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
29 bitr3 341 . . . . . . . . . . . 12 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → ([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
3029com12 32 . . . . . . . . . . 11 (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
3122, 28, 30e11 39438 . . . . . . . . . 10 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
3231gen11 39366 . . . . . . . . 9 (   𝐴𝐵   ▶   𝑦([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
33 albi 1894 . . . . . . . . 9 (∀𝑦([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
3432, 33e1a 39377 . . . . . . . 8 (   𝐴𝐵   ▶   (∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
35 sbcalgOLD 39277 . . . . . . . . 9 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)))
361, 35e1a 39377 . . . . . . . 8 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
37 bibi1 340 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → (([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) ↔ (∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
3837biimprcd 240 . . . . . . . 8 ((∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
3934, 36, 38e11 39438 . . . . . . 7 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
4039gen11 39366 . . . . . 6 (   𝐴𝐵   ▶   𝑧([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
41 albi 1894 . . . . . 6 (∀𝑧([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
4240, 41e1a 39377 . . . . 5 (   𝐴𝐵   ▶   (∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
43 sbcalgOLD 39277 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)))
441, 43e1a 39377 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
45 bibi1 340 . . . . . 6 (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) ↔ (∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
4645biimprcd 240 . . . . 5 ((∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))))
4742, 44, 46e11 39438 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))   )
48 dftr2 4888 . . . 4 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
49 biantr 807 . . . . 5 ((([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) ∧ (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))) → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴))
5049ex 397 . . . 4 (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → ((Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)) → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴)))
5147, 48, 50e10 39444 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴)   )
52 dftr2 4888 . . . . 5 (Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
5352ax-gen 1870 . . . 4 𝑥(Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
54 sbcbi 39274 . . . 4 (𝐴𝐵 → (∀𝑥(Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))))
551, 53, 54e10 39444 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))   )
56 bibi1 340 . . . 4 (([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → (([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴) ↔ ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴)))
5756biimprcd 240 . . 3 (([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ Tr 𝐴) → (([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥)) → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)))
5851, 55, 57e11 39438 . 2 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴)   )
5958in1 39312 1 (𝐴𝐵 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382  ∀wal 1629   = wceq 1631   ∈ wcel 2145  [wsbc 3587  Tr wtr 4886 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-sbc 3588  df-in 3730  df-ss 3737  df-uni 4575  df-tr 4887  df-vd1 39311 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator