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

Theorem sbc5 3324
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 3309 . 2  |-  ( [. A  /  x ]. ph  ->  A  e.  _V )
2 exsimpl 1723 . . 3  |-  ( E. x ( x  =  A  /\  ph )  ->  E. x  x  =  A )
3 isset 3084 . . 3  |-  ( A  e.  _V  <->  E. x  x  =  A )
42, 3sylibr 215 . 2  |-  ( E. x ( x  =  A  /\  ph )  ->  A  e.  _V )
5 dfsbcq2 3302 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
6 eqeq2 2437 . . . . 5  |-  ( y  =  A  ->  (
x  =  y  <->  x  =  A ) )
76anbi1d 709 . . . 4  |-  ( y  =  A  ->  (
( x  =  y  /\  ph )  <->  ( x  =  A  /\  ph )
) )
87exbidv 1762 . . 3  |-  ( y  =  A  ->  ( E. x ( x  =  y  /\  ph )  <->  E. x ( x  =  A  /\  ph )
) )
9 sb5 2229 . . 3  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
105, 8, 9vtoclbg 3140 . 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 1657   [wsb 1790    e. wcel 1872   _Vcvv 3080   [.wsbc 3299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-v 3082  df-sbc 3300
This theorem is referenced by:  sbc6g  3325  sbc7  3327  sbciegft  3330  sbccomlem  3370  csb2  3397  rexsns  4032  rexsnsOLD  4033  iunxsngf  28175  sbccom2lem  32329  pm13.192  36732  pm13.195  36735  2sbc5g  36738  iotasbc  36741  pm14.122b  36745  iotasbc5  36753
  Copyright terms: Public domain W3C validator