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 38609
Description: Virtual deduction proof of csbsng 4214. 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 4214 is csbsngVD 38609 without virtual deductions and was automatically derived from csbsngVD 38609.
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 38269 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴𝑉   )
2 sbceqg 3956 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵))
31, 2e1a 38331 . . . . . . . 8 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵)   )
4 csbconstg 3527 . . . . . . . . . 10 (𝐴𝑉𝐴 / 𝑥𝑦 = 𝑦)
51, 4e1a 38331 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴 / 𝑥𝑦 = 𝑦   )
6 eqeq1 2625 . . . . . . . . 9 (𝐴 / 𝑥𝑦 = 𝑦 → (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵))
75, 6e1a 38331 . . . . . . . 8 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
8 bibi1 341 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) ↔ (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)))
98biimprd 238 . . . . . . . 8 (([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵) → ((𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵) → ([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)))
103, 7, 9e11 38392 . . . . . . 7 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
1110gen11 38320 . . . . . 6 (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
12 abbi 2734 . . . . . . 7 (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) ↔ {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵})
1312biimpi 206 . . . . . 6 (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) → {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵})
1411, 13e1a 38331 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
15 csbabgOLD 38530 . . . . . . 7 (𝐴𝑉𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦[𝐴 / 𝑥]𝑦 = 𝐵})
1615eqcomd 2627 . . . . . 6 (𝐴𝑉 → {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵})
171, 16e1a 38331 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
18 eqeq1 2625 . . . . . 6 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} ↔ 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
1918biimpcd 239 . . . . 5 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2014, 17, 19e11 38392 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
21 df-sn 4149 . . . . . 6 {𝐵} = {𝑦𝑦 = 𝐵}
2221ax-gen 1719 . . . . 5 𝑥{𝐵} = {𝑦𝑦 = 𝐵}
23 csbeq2gOLD 38244 . . . . 5 (𝐴𝑉 → (∀𝑥{𝐵} = {𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}))
241, 22, 23e10 38398 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
25 eqeq2 2632 . . . . 5 (𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} ↔ 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2625biimpd 219 . . . 4 (𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2720, 24, 26e11 38392 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
28 df-sn 4149 . . 3 {𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}
29 eqeq2 2632 . . . 4 ({𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵} ↔ 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
3029biimprcd 240 . . 3 (𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → ({𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → 𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}))
3127, 28, 30e10 38398 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}   )
3231in1 38266 1 (𝐴𝑉𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1478   = wceq 1480  wcel 1987  {cab 2607  [wsbc 3417  csb 3514  {csn 4148
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-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-sbc 3418  df-csb 3515  df-sn 4149  df-vd1 38265
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator