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

Theorem abbi2i 2549
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 2543 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
2 abbiri.1 . 2  |-  ( x  e.  A  <->  ph )
31, 2mpgbir 1560 1  |-  A  =  { x  |  ph }
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653    e. wcel 1726   {cab 2424
This theorem is referenced by:  abid2  2555  cbvralcsf  3313  cbvreucsf  3315  cbvrabcsf  3316  symdif2  3609  dfnul2  3632  dfpr2  3832  dftp2  3856  0iin  4151  epse  4568  fv3  5747  fo1st  6369  fo2nd  6370  xp2  6387  tfrlem3  6641  mapsn  7058  ixpconstg  7074  ixp0x  7093  dfom4  7607  cardnum  7980  alephiso  7984  nnzrab  10314  nn0zrab  10315  qnnen  12818  h2hcau  22487  dfch2  22914  hhcno  23412  hhcnf  23413  pjhmopidm  23691  bdayfo  25635  fobigcup  25750  dfsingles2  25771  dfrdg4  25800  tfrqfree  25801  dfint3  25802  compeq  27632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434
  Copyright terms: Public domain W3C validator