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

Theorem abbi2i 2590
 Description: Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
abbi2i.1
Assertion
Ref Expression
abbi2i
Distinct variable group:   ,

Proof of Theorem abbi2i
StepHypRef Expression
1 abeq2 2581 . 2
2 abbi2i.1 . 2
31, 2mpgbir 1622 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818  {cab 2442 This theorem is referenced by:  abid2  2597  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  symdif2  3763  dfnul2  3786  dfpr2  4044  dftp2  4075  0iin  4388  epse  4867  fv3  5884  fo1st  6820  fo2nd  6821  xp2  6835  tfrlem3  7066  mapsn  7480  ixpconstg  7498  ixp0x  7517  dfom4  8087  cardnum  8496  alephiso  8500  nnzrab  10917  nn0zrab  10918  qnnen  13947  h2hcau  25896  dfch2  26325  hhcno  26823  hhcnf  26824  pjhmopidm  27102  bdayfo  29435  fobigcup  29550  dfsingles2  29571  dfrdg4  29600  tfrqfree  29601  dfint3  29602  compeq  31348  bj-snglinv  34530 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452
 Copyright terms: Public domain W3C validator