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

Theorem abbi2i 2407
Description: Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
abbiri.1  |-  ( x  e.  A  <->  ph )
Assertion
Ref Expression
abbi2i  |-  A  =  { x  |  ph }
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem abbi2i
StepHypRef Expression
1 abeq2 2401 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
2 abbiri.1 . 2  |-  ( x  e.  A  <->  ph )
31, 2mpgbir 1540 1  |-  A  =  { x  |  ph }
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632    e. wcel 1696   {cab 2282
This theorem is referenced by:  abid2  2413  cbvralcsf  3156  cbvreucsf  3158  cbvrabcsf  3159  symdif2  3447  dfnul2  3470  dfpr2  3669  dftp2  3692  0iin  3976  epse  4392  fv3  5557  fo1st  6155  fo2nd  6156  xp2  6173  tfrlem3  6409  mapsn  6825  ixpconstg  6841  ixp0x  6860  dfom4  7366  cardnum  7737  alephiso  7741  nnzrab  10067  nn0zrab  10068  qnnen  12508  h2hcau  21575  dfch2  22002  hhcno  22500  hhcnf  22501  pjhmopidm  22779  bdayfo  24400  fobigcup  24511  dfsingles2  24531  dfrdg4  24560  tfrqfree  24561  compeq  27744
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-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator