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 38955
Description: Virtual deduction proof of csbsng 4241. 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 4241 is csbsngVD 38955 without virtual deductions and was automatically derived from csbsngVD 38955.
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 38616 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴𝑉   )
2 sbceqg 3982 . . . . . . . . 9 (𝐴𝑉 → ([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵))
31, 2e1a 38678 . . . . . . . 8 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵)   )
4 csbconstg 3544 . . . . . . . . . 10 (𝐴𝑉𝐴 / 𝑥𝑦 = 𝑦)
51, 4e1a 38678 . . . . . . . . 9 (   𝐴𝑉   ▶   𝐴 / 𝑥𝑦 = 𝑦   )
6 eqeq1 2625 . . . . . . . . 9 (𝐴 / 𝑥𝑦 = 𝑦 → (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵))
75, 6e1a 38678 . . . . . . . 8 (   𝐴𝑉   ▶   (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
8 bibi1 341 . . . . . . . . 9 (([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵) → (([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) ↔ (𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵)))
98biimprd 238 . . . . . . . 8 (([𝐴 / 𝑥]𝑦 = 𝐵𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵) → ((𝐴 / 𝑥𝑦 = 𝐴 / 𝑥𝐵𝑦 = 𝐴 / 𝑥𝐵) → ([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)))
103, 7, 9e11 38739 . . . . . . 7 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
1110gen11 38667 . . . . . 6 (   𝐴𝑉   ▶   𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵)   )
12 abbi 2736 . . . . . . 7 (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) ↔ {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵})
1312biimpi 206 . . . . . 6 (∀𝑦([𝐴 / 𝑥]𝑦 = 𝐵𝑦 = 𝐴 / 𝑥𝐵) → {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵})
1411, 13e1a 38678 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
15 csbabgOLD 38876 . . . . . . 7 (𝐴𝑉𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦[𝐴 / 𝑥]𝑦 = 𝐵})
1615eqcomd 2627 . . . . . 6 (𝐴𝑉 → {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵})
171, 16e1a 38678 . . . . 5 (   𝐴𝑉   ▶   {𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
18 eqeq1 2625 . . . . . 6 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} ↔ 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
1918biimpcd 239 . . . . 5 ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → ({𝑦[𝐴 / 𝑥]𝑦 = 𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2014, 17, 19e11 38739 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
21 df-sn 4176 . . . . . 6 {𝐵} = {𝑦𝑦 = 𝐵}
2221ax-gen 1721 . . . . 5 𝑥{𝐵} = {𝑦𝑦 = 𝐵}
23 csbeq2gOLD 38591 . . . . 5 (𝐴𝑉 → (∀𝑥{𝐵} = {𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}))
241, 22, 23e10 38745 . . . 4 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵}   )
25 eqeq2 2632 . . . . 5 (𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} ↔ 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2625biimpd 219 . . . 4 (𝐴 / 𝑥{𝑦𝑦 = 𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = 𝐴 / 𝑥{𝑦𝑦 = 𝐵} → 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
2720, 24, 26e11 38739 . . 3 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}   )
28 df-sn 4176 . . 3 {𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}
29 eqeq2 2632 . . . 4 ({𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → (𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵} ↔ 𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵}))
3029biimprcd 240 . . 3 (𝐴 / 𝑥{𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → ({𝐴 / 𝑥𝐵} = {𝑦𝑦 = 𝐴 / 𝑥𝐵} → 𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}))
3127, 28, 30e10 38745 . 2 (   𝐴𝑉   ▶   𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵}   )
3231in1 38613 1 (𝐴𝑉𝐴 / 𝑥{𝐵} = {𝐴 / 𝑥𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1480   = wceq 1482  wcel 1989  {cab 2607  [wsbc 3433  csb 3531  {csn 4175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-sbc 3434  df-csb 3532  df-sn 4176  df-vd1 38612
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator