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

Theorem abeq2i 2531
Description: Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.)
Hypothesis
Ref Expression
abeqi.1  |-  A  =  { x  |  ph }
Assertion
Ref Expression
abeq2i  |-  ( x  e.  A  <->  ph )

Proof of Theorem abeq2i
StepHypRef Expression
1 abeqi.1 . . . 4  |-  A  =  { x  |  ph }
21a1i 11 . . 3  |-  ( T. 
->  A  =  {
x  |  ph }
)
32abeq2d 2530 . 2  |-  ( T. 
->  ( x  e.  A  <->  ph ) )
43trud 1416 1  |-  ( x  e.  A  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 186    = wceq 1407   T. wtru 1408    e. wcel 1844   {cab 2389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-12 1880  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399
This theorem is referenced by:  abeq1i  2533  rabid  2986  vex  3064  csbco  3385  csbnestgf  3792  elsn  3988  funcnv3  5632  opabiota  5914  zfrep6  6754  wfrlem2  7023  wfrlem3  7024  wfrlem4  7026  wfrdmcl  7031  tfrlem4  7084  tfrlem8  7089  tfrlem9  7090  ixpn0  7541  mapsnen  7633  sbthlem1  7667  dffi3  7927  1idpr  9439  ltexprlem1  9446  ltexprlem2  9447  ltexprlem3  9448  ltexprlem4  9449  ltexprlem6  9451  ltexprlem7  9452  reclem2pr  9458  reclem3pr  9459  reclem4pr  9460  supsrlem  9520  dissnref  20323  dissnlocfin  20324  txbas  20362  xkoccn  20414  xkoptsub  20449  xkoco1cn  20452  xkoco2cn  20453  xkoinjcn  20482  mbfi1fseqlem4  22419  avril1  25601  rnmpt2ss  27971  bnj1436  29238  bnj916  29331  bnj983  29349  bnj1083  29374  bnj1245  29410  bnj1311  29420  bnj1371  29425  bnj1398  29430  setinds  30010  frrlem2  30101  frrlem3  30102  frrlem4  30103  frrlem5e  30108  frrlem11  30112  bj-ififc  30743  bj-elsngl  31104  bj-projun  31130  bj-projval  31132  f1omptsnlem  31265  icoreresf  31282  sdclem1  31531  csbcom2fi  31829  csbgfi  31830
  Copyright terms: Public domain W3C validator