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

Theorem trsbc 43766
Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 43766 is trsbcVD 44103 without virtual deductions and was automatically derived from trsbcVD 44103 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
trsbc (𝐴𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem trsbc
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sbcal 3841 . . 3 ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2 sbcal 3841 . . . . 5 ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
3 sbcim2g 43764 . . . . . . . 8 (𝐴𝑉 → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥))))
4 sbcg 3856 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦))
5 sbcel2gv 3849 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝑥𝑦𝐴))
6 sbcel2gv 3849 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝑥𝑧𝐴))
7 imbi13 43746 . . . . . . . . 9 (([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) → (([𝐴 / 𝑥]𝑦𝑥𝑦𝐴) → (([𝐴 / 𝑥]𝑧𝑥𝑧𝐴) → (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))))))
84, 5, 6, 7syl3c 66 . . . . . . . 8 (𝐴𝑉 → (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))))
93, 8bitrd 279 . . . . . . 7 (𝐴𝑉 → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))))
10 pm3.31 449 . . . . . . . . 9 ((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
11 pm3.3 448 . . . . . . . . 9 (((𝑧𝑦𝑦𝑥) → 𝑧𝑥) → (𝑧𝑦 → (𝑦𝑥𝑧𝑥)))
1210, 11impbii 208 . . . . . . . 8 ((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
1312sbcbii 3837 . . . . . . 7 ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
14 pm3.31 449 . . . . . . . 8 ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
15 pm3.3 448 . . . . . . . 8 (((𝑧𝑦𝑦𝐴) → 𝑧𝐴) → (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))
1614, 15impbii 208 . . . . . . 7 ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
179, 13, 163bitr3g 313 . . . . . 6 (𝐴𝑉 → ([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
1817albidv 1922 . . . . 5 (𝐴𝑉 → (∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
192, 18bitrid 283 . . . 4 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
2019albidv 1922 . . 3 (𝐴𝑉 → (∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
211, 20bitrid 283 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
22 dftr2 5267 . . 3 (Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2322sbcbii 3837 . 2 ([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
24 dftr2 5267 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
2521, 23, 243bitr4g 314 1 (𝐴𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wal 1538  wcel 2105  [wsbc 3777  Tr wtr 5265
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-sbc 3778  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266
This theorem is referenced by:  truniALT  43767  truniALTVD  44104  trintALTVD  44106  trintALT  44107
  Copyright terms: Public domain W3C validator