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

Theorem sbc5 3330
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 3315 . 2  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
2 exsimpl 1724 . . 3  |-  ( E. x ( x  =  A  /\  ph )  ->  E. x  x  =  A )
3 isset 3091 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
42, 3sylibr 215 . 2  |-  ( E. x ( x  =  A  /\  ph )  ->  A  e.  _V )
5 dfsbcq2 3308 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
6 eqeq2 2444 . . . . 5  |-  ( y  =  A  ->  (
x  =  y  <->  x  =  A ) )
76anbi1d 709 . . . 4  |-  ( y  =  A  ->  (
( x  =  y  /\  ph )  <->  ( x  =  A  /\  ph )
) )
87exbidv 1761 . . 3  |-  ( y  =  A  ->  ( E. x ( x  =  y  /\  ph )  <->  E. x ( x  =  A  /\  ph )
) )
9 sb5 2226 . . 3  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
105, 8, 9vtoclbg 3146 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) ) )
111, 4, 10pm5.21nii 354 1  |-  ( [. A  /  x ]. ph  <->  E. x
( x  =  A  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    = wceq 1437   E.wex 1659   [wsb 1789    e. wcel 1870   _Vcvv 3087   [.wsbc 3305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-v 3089  df-sbc 3306
This theorem is referenced by:  sbc6g  3331  sbc7  3333  sbciegft  3336  sbccomlem  3376  csb2  3403  rexsns  4035  rexsnsOLD  4036  iunxsngf  28011  sbccom2lem  32068  pm13.192  36398  pm13.195  36401  2sbc5g  36404  iotasbc  36407  pm14.122b  36411  iotasbc5  36419
  Copyright terms: Public domain W3C validator