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

Theorem sbcoreleleqVD 38578
Description: Virtual deduction proof of sbcoreleleq 38227. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:1,?: e1a 38334 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑥 𝑦𝑥𝐴)   )
3:1,?: e1a 38334 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑦 𝑥𝐴𝑥)   )
4:1,?: e1a 38334 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑥 = 𝑦𝑥 = 𝐴)   )
5:2,3,4,?: e111 38381 (   𝐴𝐵   ▶   ((𝑥𝐴 𝐴𝑥𝑥 = 𝐴) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥 [𝐴 / 𝑦]𝑥 = 𝑦))   )
6:1,?: e1a 38334 (   𝐴𝐵    ▶   ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ ([𝐴 / 𝑦]𝑥 𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦))   )
7:5,6: e11 38395 (   𝐴𝐵   ▶   ([𝐴 / 𝑦](𝑥 𝑦𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴))   )
qed:7: (𝐴𝐵 → ([𝐴 / 𝑦](𝑥𝑦 𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sbcoreleleqVD (𝐴𝐵 → ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴)))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem sbcoreleleqVD
StepHypRef Expression
1 idn1 38272 . . . . 5 (   𝐴𝐵   ▶   𝐴𝐵   )
2 sbcel2gv 3478 . . . . 5 (𝐴𝐵 → ([𝐴 / 𝑦]𝑥𝑦𝑥𝐴))
31, 2e1a 38334 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑥𝑦𝑥𝐴)   )
4 sbcel1gvOLD 38577 . . . . 5 (𝐴𝐵 → ([𝐴 / 𝑦]𝑦𝑥𝐴𝑥))
51, 4e1a 38334 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑦𝑥𝐴𝑥)   )
6 eqsbc3r 3474 . . . . 5 (𝐴𝐵 → ([𝐴 / 𝑦]𝑥 = 𝑦𝑥 = 𝐴))
71, 6e1a 38334 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑦]𝑥 = 𝑦𝑥 = 𝐴)   )
8 3orbi123 38199 . . . . 5 ((([𝐴 / 𝑦]𝑥𝑦𝑥𝐴) ∧ ([𝐴 / 𝑦]𝑦𝑥𝐴𝑥) ∧ ([𝐴 / 𝑦]𝑥 = 𝑦𝑥 = 𝐴)) → (([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴)))
983impexpbicomi 38168 . . . 4 (([𝐴 / 𝑦]𝑥𝑦𝑥𝐴) → (([𝐴 / 𝑦]𝑦𝑥𝐴𝑥) → (([𝐴 / 𝑦]𝑥 = 𝑦𝑥 = 𝐴) → ((𝑥𝐴𝐴𝑥𝑥 = 𝐴) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦)))))
103, 5, 7, 9e111 38381 . . 3 (   𝐴𝐵   ▶   ((𝑥𝐴𝐴𝑥𝑥 = 𝐴) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦))   )
11 sbc3orgOLD 38224 . . . 4 (𝐴𝐵 → ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦)))
121, 11e1a 38334 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦))   )
13 biantr 971 . . . 4 ((([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦)) ∧ ((𝑥𝐴𝐴𝑥𝑥 = 𝐴) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦))) → ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴)))
1413expcom 451 . . 3 (((𝑥𝐴𝐴𝑥𝑥 = 𝐴) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦)) → (([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ ([𝐴 / 𝑦]𝑥𝑦[𝐴 / 𝑦]𝑦𝑥[𝐴 / 𝑦]𝑥 = 𝑦)) → ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴))))
1510, 12, 14e11 38395 . 2 (   𝐴𝐵   ▶   ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴))   )
1615in1 38269 1 (𝐴𝐵 → ([𝐴 / 𝑦](𝑥𝑦𝑦𝑥𝑥 = 𝑦) ↔ (𝑥𝐴𝐴𝑥𝑥 = 𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3o 1035   = wceq 1480  wcel 1987  [wsbc 3417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3188  df-sbc 3418  df-vd1 38268
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator