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 44918
Description: Virtual deduction proof of csbsng 4707. 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 4707 is csbsngVD 44918 without virtual deductions and was automatically derived from csbsngVD 44918.
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 44599 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴𝑉   )
2 sbceqg 4411 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵))
31, 2e1a 44652 . . . . . . . 8 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵)   )
4 csbconstg 3917 . . . . . . . . . 10 (𝐴𝑉𝐴 / 𝑥𝑦 = 𝑦)
51, 4e1a 44652 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴 / 𝑥𝑦 = 𝑦   )
6 eqeq1 2740 . . . . . . . . 9 (𝐴 / 𝑥𝑦 = 𝑦 → (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵))
75, 6e1a 44652 . . . . . . . 8 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
8 bibi1 351 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) ↔ (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)))
98biimprd 248 . . . . . . . 8 (([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵) → ((𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵) → ([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)))
103, 7, 9e11 44713 . . . . . . 7 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
1110gen11 44641 . . . . . 6 (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
12 abbib 2810 . . . . . . 7 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} ↔ ∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵))
1312biimpri 228 . . . . . 6 (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) → {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵})
1411, 13e1a 44652 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
15 csbab 4439 . . . . . . . 8 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦[𝐴 / 𝑥]𝑦 = 𝐵}
1615a1i 11 . . . . . . 7 (𝐴𝑉𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦[𝐴 / 𝑥]𝑦 = 𝐵})
1716eqcomd 2742 . . . . . 6 (𝐴𝑉 → {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵})
181, 17e1a 44652 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
19 eqeq1 2740 . . . . . 6 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} ↔ 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2019biimpcd 249 . . . . 5 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2114, 18, 20e11 44713 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
22 df-sn 4626 . . . . . 6 {𝐵} = {𝑦𝑦 = 𝐵}
2322ax-gen 1794 . . . . 5 𝑥{𝐵} = {𝑦𝑦 = 𝐵}
24 csbeq2 3903 . . . . . 6 (∀𝑥{𝐵} = {𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵})
2524a1i 11 . . . . 5 (𝐴𝑉 → (∀𝑥{𝐵} = {𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}))
261, 23, 25e10 44719 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
27 eqeq2 2748 . . . . 5 (𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} ↔ 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2827biimpd 229 . . . 4 (𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2921, 26, 28e11 44713 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
30 df-sn 4626 . . 3 {𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}
31 eqeq2 2748 . . . 4 ({𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵} ↔ 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
3231biimprcd 250 . . 3 (𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → ({𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → 𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}))
3329, 30, 32e10 44719 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}   )
3433in1 44596 1 (𝐴𝑉𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1537   = wceq 1539  wcel 2107  {cab 2713  [wsbc 3787  csb 3898  {csn 4625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-nul 4333  df-sn 4626  df-vd1 44595
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator