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

Theorem sbcssgVD 38939
Description: Virtual deduction proof of sbcssg 4076. 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. sbcssg 4076 is sbcssgVD 38939 without virtual deductions and was automatically derived from sbcssgVD 38939.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐶𝑦 𝐴 / 𝑥𝐶)   )
3:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐷𝑦 𝐴 / 𝑥𝐷)   )
4:2,3: (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝑦𝐶 [𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷 ))   )
5:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶 𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷))   )
6:4,5: (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶 𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
7:6: (   𝐴𝐵   ▶   𝑦([𝐴 / 𝑥](𝑦 𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
8:7: (   𝐴𝐵   ▶   (∀𝑦[𝐴 / 𝑥](𝑦 𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷) )   )
9:1: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦(𝑦 𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷))   )
10:8,9: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦(𝑦 𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷) )   )
11:: (𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦𝐷))
110:11: 𝑥(𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦 𝐷))
12:1,110: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷 [𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷))   )
13:10,12: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷 𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
14:: (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷 ↔ ∀ 𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))
15:13,14: (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷 𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷)   )
qed:15: (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷 𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sbcssgVD (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))

Proof of Theorem sbcssgVD
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 idn1 38610 . . . . . . . . . 10 (   𝐴𝐵   ▶   𝐴𝐵   )
2 sbcel2gOLD 38575 . . . . . . . . . 10 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶))
31, 2e1a 38672 . . . . . . . . 9 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶)   )
4 sbcel2gOLD 38575 . . . . . . . . . 10 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦𝐷𝑦𝐴 / 𝑥𝐷))
51, 4e1a 38672 . . . . . . . . 9 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐷𝑦𝐴 / 𝑥𝐷)   )
6 imbi12 336 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶) → (([𝐴 / 𝑥]𝑦𝐷𝑦𝐴 / 𝑥𝐷) → (([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
73, 5, 6e11 38733 . . . . . . . 8 (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
8 sbcimg 3471 . . . . . . . . 9 (𝐴𝐵 → ([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷)))
91, 8e1a 38672 . . . . . . . 8 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷))   )
10 bibi1 341 . . . . . . . . 9 (([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷)) → (([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) ↔ (([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
1110biimprcd 240 . . . . . . . 8 ((([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → (([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷)) → ([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
127, 9, 11e11 38733 . . . . . . 7 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
1312gen11 38661 . . . . . 6 (   𝐴𝐵   ▶   𝑦([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
14 albi 1744 . . . . . 6 (∀𝑦([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → (∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)))
1513, 14e1a 38672 . . . . 5 (   𝐴𝐵   ▶   (∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
16 sbcalgOLD 38572 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷)))
171, 16e1a 38672 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷))   )
18 bibi1 341 . . . . . 6 (([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷)) → (([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) ↔ (∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
1918biimprcd 240 . . . . 5 ((∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → (([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷)) → ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
2015, 17, 19e11 38733 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
21 dfss2 3584 . . . . . 6 (𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦𝐷))
2221ax-gen 1720 . . . . 5 𝑥(𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦𝐷))
23 sbcbi 38569 . . . . 5 (𝐴𝐵 → (∀𝑥(𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦𝐷)) → ([𝐴 / 𝑥]𝐶𝐷[𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷))))
241, 22, 23e10 38739 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷[𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷))   )
25 bibi1 341 . . . . 5 (([𝐴 / 𝑥]𝐶𝐷[𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷)) → (([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) ↔ ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
2625biimprcd 240 . . . 4 (([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → (([𝐴 / 𝑥]𝐶𝐷[𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷)) → ([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
2720, 24, 26e11 38733 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
28 dfss2 3584 . . 3 (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))
29 biantr 971 . . . 4 ((([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) ∧ (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))) → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
3029ex 450 . . 3 (([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → ((𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷)))
3127, 28, 30e10 38739 . 2 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷)   )
3231in1 38607 1 (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1479  wcel 1988  [wsbc 3429  csb 3526  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-sbc 3430  df-csb 3527  df-in 3574  df-ss 3581  df-vd1 38606
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator