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

Theorem csbeq2gVD 44115
Description: Virtual deduction proof of csbeq2 3898. 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. csbeq2 3898 is csbeq2gVD 44115 without virtual deductions and was automatically derived from csbeq2gVD 44115.
1:: (   𝐴𝑉   ▶   𝐴𝑉   )
2:1: (   𝐴𝑉   ▶   (∀𝑥𝐵 = 𝐶[𝐴 / 𝑥] 𝐵 = 𝐶)   )
3:1: (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)   )
4:2,3: (   𝐴𝑉   ▶   (∀𝑥𝐵 = 𝐶𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐶)   )
qed:4: (𝐴𝑉 → (∀𝑥𝐵 = 𝐶𝐴 / 𝑥 𝐵 = 𝐴 / 𝑥𝐶))
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbeq2gVD (𝐴𝑉 → (∀𝑥 𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶))

Proof of Theorem csbeq2gVD
StepHypRef Expression
1 idn1 43797 . . . 4 (   𝐴𝑉   ▶   𝐴𝑉   )
2 spsbc 3790 . . . 4 (𝐴𝑉 → (∀𝑥 𝐵 = 𝐶[𝐴 / 𝑥]𝐵 = 𝐶))
31, 2e1a 43850 . . 3 (   𝐴𝑉   ▶   (∀𝑥 𝐵 = 𝐶[𝐴 / 𝑥]𝐵 = 𝐶)   )
4 sbceqg 4409 . . . 4 (𝐴𝑉 → ([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶))
51, 4e1a 43850 . . 3 (   𝐴𝑉   ▶   ([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)   )
6 imbi2 348 . . . 4 (([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶) → ((∀𝑥 𝐵 = 𝐶[𝐴 / 𝑥]𝐵 = 𝐶) ↔ (∀𝑥 𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)))
76biimpcd 248 . . 3 ((∀𝑥 𝐵 = 𝐶[𝐴 / 𝑥]𝐵 = 𝐶) → (([𝐴 / 𝑥]𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶) → (∀𝑥 𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)))
83, 5, 7e11 43911 . 2 (   𝐴𝑉   ▶   (∀𝑥 𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶)   )
98in1 43794 1 (𝐴𝑉 → (∀𝑥 𝐵 = 𝐶𝐴 / 𝑥𝐵 = 𝐴 / 𝑥𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1538   = wceq 1540  wcel 2105  [wsbc 3777  csb 3893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-sbc 3778  df-csb 3894  df-vd1 43793
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator