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

Theorem sbc5 3304
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 3289 . 2  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
2 exsimpl 1740 . . 3  |-  ( E. x ( x  =  A  /\  ph )  ->  E. x  x  =  A )
3 isset 3061 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
42, 3sylibr 217 . 2  |-  ( E. x ( x  =  A  /\  ph )  ->  A  e.  _V )
5 dfsbcq2 3282 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
6 eqeq2 2473 . . . . 5  |-  ( y  =  A  ->  (
x  =  y  <->  x  =  A ) )
76anbi1d 716 . . . 4  |-  ( y  =  A  ->  (
( x  =  y  /\  ph )  <->  ( x  =  A  /\  ph )
) )
87exbidv 1779 . . 3  |-  ( y  =  A  ->  ( E. x ( x  =  y  /\  ph )  <->  E. x ( x  =  A  /\  ph )
) )
9 sb5 2270 . . 3  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
105, 8, 9vtoclbg 3120 . 2  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) ) )
111, 4, 10pm5.21nii 359 1  |-  ( [. A  /  x ]. ph  <->  E. x
( x  =  A  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375    = wceq 1455   E.wex 1674   [wsb 1808    e. wcel 1898   _Vcvv 3057   [.wsbc 3279
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-v 3059  df-sbc 3280
This theorem is referenced by:  sbc6g  3305  sbc7  3307  sbciegft  3310  sbccomlem  3350  csb2  3377  rexsns  4016  rexsnsOLD  4017  iunxsngf  28227  sbccom2lem  32410  pm13.192  36806  pm13.195  36809  2sbc5g  36812  iotasbc  36815  pm14.122b  36819  iotasbc5  36827
  Copyright terms: Public domain W3C validator