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 44464
Description: Virtual deduction proof of sbcssg 4525. 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 4525 is sbcssgVD 44464 without virtual deductions and was automatically derived from sbcssgVD 44464.
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 44155 . . . . . . . . . 10 (   𝐴𝐵   ▶   𝐴𝐵   )
2 sbcel2 4417 . . . . . . . . . . 11 ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶)
32a1i 11 . . . . . . . . . 10 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶))
41, 3e1a 44208 . . . . . . . . 9 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶)   )
5 sbcel2 4417 . . . . . . . . . . 11 ([𝐴 / 𝑥]𝑦𝐷𝑦𝐴 / 𝑥𝐷)
65a1i 11 . . . . . . . . . 10 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦𝐷𝑦𝐴 / 𝑥𝐷))
71, 6e1a 44208 . . . . . . . . 9 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦𝐷𝑦𝐴 / 𝑥𝐷)   )
8 imbi12 345 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦𝐶𝑦𝐴 / 𝑥𝐶) → (([𝐴 / 𝑥]𝑦𝐷𝑦𝐴 / 𝑥𝐷) → (([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
94, 7, 8e11 44269 . . . . . . . 8 (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
10 sbcimg 3825 . . . . . . . . 9 (𝐴𝐵 → ([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷)))
111, 10e1a 44208 . . . . . . . 8 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷))   )
12 bibi1 350 . . . . . . . . 9 (([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷)) → (([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) ↔ (([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
1312biimprcd 249 . . . . . . . 8 ((([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → (([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ([𝐴 / 𝑥]𝑦𝐶[𝐴 / 𝑥]𝑦𝐷)) → ([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
149, 11, 13e11 44269 . . . . . . 7 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
1514gen11 44197 . . . . . 6 (   𝐴𝐵   ▶   𝑦([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
16 albi 1812 . . . . . 6 (∀𝑦([𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ (𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → (∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)))
1715, 16e1a 44208 . . . . 5 (   𝐴𝐵   ▶   (∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
18 sbcal 3837 . . . . . . 7 ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷))
1918a1i 11 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷)))
201, 19e1a 44208 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷))   )
21 bibi1 350 . . . . . 6 (([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷)) → (([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) ↔ (∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
2221biimprcd 249 . . . . 5 ((∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → (([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦[𝐴 / 𝑥](𝑦𝐶𝑦𝐷)) → ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
2317, 20, 22e11 44269 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
24 df-ss 3961 . . . . . 6 (𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦𝐷))
2524ax-gen 1789 . . . . 5 𝑥(𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦𝐷))
26 sbcbi 44120 . . . . 5 (𝐴𝐵 → (∀𝑥(𝐶𝐷 ↔ ∀𝑦(𝑦𝐶𝑦𝐷)) → ([𝐴 / 𝑥]𝐶𝐷[𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷))))
271, 25, 26e10 44275 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷[𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷))   )
28 bibi1 350 . . . . 5 (([𝐴 / 𝑥]𝐶𝐷[𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷)) → (([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) ↔ ([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
2928biimprcd 249 . . . 4 (([𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷) ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → (([𝐴 / 𝑥]𝐶𝐷[𝐴 / 𝑥]𝑦(𝑦𝐶𝑦𝐷)) → ([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))))
3023, 27, 29e11 44269 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))   )
31 df-ss 3961 . . 3 (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))
32 biantr 804 . . . 4 ((([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) ∧ (𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷))) → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
3332ex 411 . . 3 (([𝐴 / 𝑥]𝐶𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → ((𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷 ↔ ∀𝑦(𝑦𝐴 / 𝑥𝐶𝑦𝐴 / 𝑥𝐷)) → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷)))
3430, 31, 33e10 44275 . 2 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷)   )
3534in1 44152 1 (𝐴𝐵 → ([𝐴 / 𝑥]𝐶𝐷𝐴 / 𝑥𝐶𝐴 / 𝑥𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1531  wcel 2098  [wsbc 3773  csb 3889  wss 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-ss 3961  df-nul 4323  df-vd1 44151
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator