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

Theorem abbi2i 2394
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 2388 . 2  |-  ( A  =  { x  | 
ph }  <->  A. x
( x  e.  A  <->  ph ) )
2 abbiri.1 . 2  |-  ( x  e.  A  <->  ph )
31, 2mpgbir 1537 1  |-  A  =  { x  |  ph }
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1684   {cab 2269
This theorem is referenced by:  abid2  2400  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  symdif2  3434  dfnul2  3457  dfpr2  3656  dftp2  3679  0iin  3960  epse  4376  fv3  5541  fo1st  6139  fo2nd  6140  xp2  6157  tfrlem3  6393  mapsn  6809  ixpconstg  6825  ixp0x  6844  dfom4  7350  cardnum  7721  alephiso  7725  nnzrab  10051  nn0zrab  10052  qnnen  12492  h2hcau  21559  dfch2  21986  hhcno  22484  hhcnf  22485  pjhmopidm  22763  bdayfo  24329  fobigcup  24440  dfsingles2  24460  dfrdg4  24488  tfrqfree  24489  compeq  27641
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator