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

Theorem csbsngVD 39876
Description: Virtual deduction proof of csbsng 4431. 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. csbsng 4431 is csbsngVD 39876 without virtual deductions and was automatically derived from csbsngVD 39876.
1:: (   𝐴𝑉   ▶   𝐴𝑉   )
2:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵)   )
3:1: (   𝐴𝑉   ▶   𝐴 / 𝑥𝑦 = 𝑦   )
4:3: (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
5:2,4: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵 𝑦 = 𝐴 / 𝑥𝐵)   )
6:5: (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
7:6: (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
8:1: (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
9:7,8: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
10:: {𝐵} = {𝑦𝑦 = 𝐵}
11:10: 𝑥{𝐵} = {𝑦𝑦 = 𝐵}
12:1,11: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
13:9,12: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = { 𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
14:: {𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}
15:13,14: (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = { 𝐴 / 𝑥𝐵}   )
qed:15: (𝐴𝑉𝐴 / 𝑥{𝐵} = { 𝐴 / 𝑥𝐵})
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbsngVD (𝐴𝑉𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})

Proof of Theorem csbsngVD
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 idn1 39547 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴𝑉   )
2 sbceqg 4177 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵))
31, 2e1a 39609 . . . . . . . 8 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵)   )
4 csbconstg 3739 . . . . . . . . . 10 (𝐴𝑉𝐴 / 𝑥𝑦 = 𝑦)
51, 4e1a 39609 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴 / 𝑥𝑦 = 𝑦   )
6 eqeq1 2801 . . . . . . . . 9 (𝐴 / 𝑥𝑦 = 𝑦 → (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵))
75, 6e1a 39609 . . . . . . . 8 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
8 bibi1 343 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) ↔ (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)))
98biimprd 240 . . . . . . . 8 (([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵) → ((𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵) → ([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)))
103, 7, 9e11 39670 . . . . . . 7 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
1110gen11 39598 . . . . . 6 (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
12 abbi 2912 . . . . . . 7 (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) ↔ {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵})
1312biimpi 208 . . . . . 6 (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) → {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵})
1411, 13e1a 39609 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
15 csbab 4202 . . . . . . . 8 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦[𝐴 / 𝑥]𝑦 = 𝐵}
1615a1i 11 . . . . . . 7 (𝐴𝑉𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦[𝐴 / 𝑥]𝑦 = 𝐵})
1716eqcomd 2803 . . . . . 6 (𝐴𝑉 → {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵})
181, 17e1a 39609 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
19 eqeq1 2801 . . . . . 6 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} ↔ 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2019biimpcd 241 . . . . 5 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2114, 18, 20e11 39670 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
22 df-sn 4367 . . . . . 6 {𝐵} = {𝑦𝑦 = 𝐵}
2322ax-gen 1891 . . . . 5 𝑥{𝐵} = {𝑦𝑦 = 𝐵}
24 csbeq2 3730 . . . . . 6 (∀𝑥{𝐵} = {𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵})
2524a1i 11 . . . . 5 (𝐴𝑉 → (∀𝑥{𝐵} = {𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}))
261, 23, 25e10 39676 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
27 eqeq2 2808 . . . . 5 (𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} ↔ 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2827biimpd 221 . . . 4 (𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2921, 26, 28e11 39670 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
30 df-sn 4367 . . 3 {𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}
31 eqeq2 2808 . . . 4 ({𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵} ↔ 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
3231biimprcd 242 . . 3 (𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → ({𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → 𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}))
3329, 30, 32e10 39676 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}   )
3433in1 39544 1 (𝐴𝑉𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1651   = wceq 1653  wcel 2157  {cab 2783  [wsbc 3631  csb 3726  {csn 4366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2375  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-nul 4114  df-sn 4367  df-vd1 39543
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator