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

Theorem csbeq2gVD 33173
Description: Virtual deduction proof of csbeq2gOLD 32803. 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. csbeq2gOLD 32803 is csbeq2gVD 33173 without virtual deductions and was automatically derived from csbeq2gVD 33173.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  ( A. x B  =  C  ->  [. A  /  x ].  B  =  C ) ).
3:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) ).
4:2,3:  |-  (. A  e.  V  ->.  ( A. x B  =  C  ->  [_ A  /  x  ]_ B  =  [_ A  /  x ]_ C ) ).
qed:4:  |-  ( A  e.  V  ->  ( A. x B  =  C  ->  [_ A  /  x ]_  B  =  [_ A  /  x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbeq2gVD  |-  ( A  e.  V  ->  ( A. x  B  =  C  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) )

Proof of Theorem csbeq2gVD
StepHypRef Expression
1 idn1 32832 . . . 4  |-  (. A  e.  V  ->.  A  e.  V ).
2 spsbc 3349 . . . 4  |-  ( A  e.  V  ->  ( A. x  B  =  C  ->  [. A  /  x ]. B  =  C
) )
31, 2e1a 32894 . . 3  |-  (. A  e.  V  ->.  ( A. x  B  =  C  ->  [. A  /  x ]. B  =  C ) ).
4 sbceqg 3830 . . . 4  |-  ( A  e.  V  ->  ( [. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) )
51, 4e1a 32894 . . 3  |-  (. A  e.  V  ->.  ( [. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) ).
6 imbi2 324 . . . 4  |-  ( (
[. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )  -> 
( ( A. x  B  =  C  ->  [. A  /  x ]. B  =  C )  <->  ( A. x  B  =  C  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C
) ) )
76biimpcd 224 . . 3  |-  ( ( A. x  B  =  C  ->  [. A  /  x ]. B  =  C )  ->  ( ( [. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C )  -> 
( A. x  B  =  C  ->  [_ A  /  x ]_ B  = 
[_ A  /  x ]_ C ) ) )
83, 5, 7e11 32955 . 2  |-  (. A  e.  V  ->.  ( A. x  B  =  C  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) ).
98in1 32829 1  |-  ( A  e.  V  ->  ( A. x  B  =  C  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377    = wceq 1379    e. wcel 1767   [.wsbc 3336   [_csb 3440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-sbc 3337  df-csb 3441  df-vd1 32828
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator