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 43301
Description: Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 43301 is trsbcVD 43638 without virtual deductions and was automatically derived from trsbcVD 43638 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 3842 . . 3 ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2 sbcal 3842 . . . . 5 ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
3 sbcim2g 43299 . . . . . . . 8 (𝐴𝑉 → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥))))
4 sbcg 3857 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝑦𝑧𝑦))
5 sbcel2gv 3850 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦𝑥𝑦𝐴))
6 sbcel2gv 3850 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝑥𝑧𝐴))
7 imbi13 43281 . . . . . . . . 9 (([𝐴 / 𝑥]𝑧𝑦𝑧𝑦) → (([𝐴 / 𝑥]𝑦𝑥𝑦𝐴) → (([𝐴 / 𝑥]𝑧𝑥𝑧𝐴) → (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))))))
84, 5, 6, 7syl3c 66 . . . . . . . 8 (𝐴𝑉 → (([𝐴 / 𝑥]𝑧𝑦 → ([𝐴 / 𝑥]𝑦𝑥[𝐴 / 𝑥]𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))))
93, 8bitrd 279 . . . . . . 7 (𝐴𝑉 → ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ (𝑧𝑦 → (𝑦𝐴𝑧𝐴))))
10 pm3.31 451 . . . . . . . . 9 ((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) → ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
11 pm3.3 450 . . . . . . . . 9 (((𝑧𝑦𝑦𝑥) → 𝑧𝑥) → (𝑧𝑦 → (𝑦𝑥𝑧𝑥)))
1210, 11impbii 208 . . . . . . . 8 ((𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ ((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
1312sbcbii 3838 . . . . . . 7 ([𝐴 / 𝑥](𝑧𝑦 → (𝑦𝑥𝑧𝑥)) ↔ [𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
14 pm3.31 451 . . . . . . . 8 ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
15 pm3.3 450 . . . . . . . 8 (((𝑧𝑦𝑦𝐴) → 𝑧𝐴) → (𝑧𝑦 → (𝑦𝐴𝑧𝐴)))
1614, 15impbii 208 . . . . . . 7 ((𝑧𝑦 → (𝑦𝐴𝑧𝐴)) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
179, 13, 163bitr3g 313 . . . . . 6 (𝐴𝑉 → ([𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
1817albidv 1924 . . . . 5 (𝐴𝑉 → (∀𝑦[𝐴 / 𝑥]((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
192, 18bitrid 283 . . . 4 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
2019albidv 1924 . . 3 (𝐴𝑉 → (∀𝑧[𝐴 / 𝑥]𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
211, 20bitrid 283 . 2 (𝐴𝑉 → ([𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥) ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴)))
22 dftr2 5268 . . 3 (Tr 𝑥 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
2322sbcbii 3838 . 2 ([𝐴 / 𝑥]Tr 𝑥[𝐴 / 𝑥]𝑧𝑦((𝑧𝑦𝑦𝑥) → 𝑧𝑥))
24 dftr2 5268 . 2 (Tr 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
2521, 23, 243bitr4g 314 1 (𝐴𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540  wcel 2107  [wsbc 3778  Tr wtr 5266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sbc 3779  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267
This theorem is referenced by:  truniALT  43302  truniALTVD  43639  trintALTVD  43641  trintALT  43642
  Copyright terms: Public domain W3C validator