MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbc5 Unicode version

Theorem sbc5 3028
Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993.) (Revised by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
sbc5  |-  ( [. A  /  x ]. ph  <->  E. x
( x  =  A  /\  ph ) )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem sbc5
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 sbcex 3013 . 2  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
2 exsimpl 1582 . . 3  |-  ( E. x ( x  =  A  /\  ph )  ->  E. x  x  =  A )
3 isset 2805 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
42, 3sylibr 203 . 2  |-  ( E. x ( x  =  A  /\  ph )  ->  A  e.  _V )
5 dfsbcq2 3007 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
6 eqeq2 2305 . . . . 5  |-  ( y  =  A  ->  (
x  =  y  <->  x  =  A ) )
76anbi1d 685 . . . 4  |-  ( y  =  A  ->  (
( x  =  y  /\  ph )  <->  ( x  =  A  /\  ph )
) )
87exbidv 1616 . . 3  |-  ( y  =  A  ->  ( E. x ( x  =  y  /\  ph )  <->  E. x ( x  =  A  /\  ph )
) )
9 sb5 2052 . . 3  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
105, 8, 9vtoclbg 2857 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) ) )
111, 4, 10pm5.21nii 342 1  |-  ( [. A  /  x ]. ph  <->  E. x
( x  =  A  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531    = wceq 1632   [wsb 1638    e. wcel 1696   _Vcvv 2801   [.wsbc 3004
This theorem is referenced by:  sbc6g  3029  sbc7  3031  sbciegft  3034  sbccomlem  3074  csb2  3096  rexsns  3684  pm13.192  27713  pm13.195  27716  2sbc5g  27719  iotasbc  27722  pm14.122b  27726  iotasbc5  27734  bnj1465  29193
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sbc 3005
  Copyright terms: Public domain W3C validator