MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abbii Structured version   Visualization version   GIF version

Theorem abbii 2882
Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
abbii.1 (𝜑𝜓)
Assertion
Ref Expression
abbii {𝑥𝜑} = {𝑥𝜓}

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2880 . 2 (∀𝑥(𝜑𝜓) ↔ {𝑥𝜑} = {𝑥𝜓})
2 abbii.1 . 2 (𝜑𝜓)
31, 2mpgbi 1893 1 {𝑥𝜑} = {𝑥𝜓}
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652  {cab 2751
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761
This theorem is referenced by:  rabrab  3264  rabswap  3269  rabbiia  3333  rabab  3376  csb2  3695  cbvcsb  3698  csbid  3701  csbco  3703  cbvreucsf  3727  unrab  4064  inrab  4065  inrab2  4066  difrab  4067  rabun2  4072  dfnul3  4084  dfif2  4247  dfsn2ALT  4356  rabsnifsb  4414  tprot  4441  pw0  4499  pwpw0  4500  dfopif  4558  pwsn  4588  pwsnALT  4589  dfuni2  4598  unipr  4609  dfint2  4637  dfiunv2  4714  cbviun  4715  cbviin  4716  iunrab  4725  iunid  4733  viin  4737  iinuni  4768  cbvopab  4882  cbvopab1  4884  cbvopab2  4885  cbvopab1s  4886  cbvopab2v  4888  unopab  4889  zfrep4  4941  zfpair  5062  iunopab  5175  dfid3  5188  rabxp  5324  csbxp  5372  dfdm3  5480  dfrn2  5481  dfrn3  5482  dfdm4  5486  dfdmf  5487  csbdm  5488  dmun  5501  dmopab  5505  dmopabss  5506  dmopab3  5507  dfrnf  5535  rnopab  5541  rnmpt  5542  dfima2  5652  dfima3  5653  imadmrn  5660  imai  5662  args  5677  mptpreima  5816  dfiota2  6034  cbviota  6038  sb8iota  6040  mptfnf  6195  dffv4  6374  dfimafn2  6437  opabiotadm  6451  fndmin  6516  fnasrn  6604  elabrex  6695  abrexco  6696  dfoprab2  6901  cbvoprab2  6928  dmoprab  6941  rnoprab  6943  rnoprab2  6944  fnrnov  7007  abnex  7165  uniuni  7171  zfrep6  7334  fvresex  7339  abrexex2g  7344  abexssex  7349  abrexex2OLD  7350  abexex  7351  oprabrexex2  7358  dfopab2  7424  suppvalbr  7503  cnvimadfsn  7508  dfrecs3  7675  rdglem1  7717  snec  8015  pmex  8067  dfixp  8117  cbvixp  8132  marypha2lem4  8553  ruv  8716  tcsni  8836  scottexs  8967  scott0s  8968  kardex  8974  cardf2  9022  dfac3  9197  infmap2  9295  cf0  9328  cfval2  9337  isf33lem  9443  dffin1-5  9465  axdc2lem  9525  addcompr  10098  mulcompr  10100  dfnn3  11292  hashf1lem2  13444  prprrab  13459  cshwsexa  13856  trclun  14043  shftdm  14099  hashbc0  15991  lubfval  17247  glbfval  17260  oduglb  17408  odulub  17410  symgbas0  18080  pmtrprfvalrn  18174  efgval2  18404  dvdsrval  18915  dfrhm2  18989  toponsspwpw  21009  tgval2  21043  tgdif0  21079  xkobval  21672  ustfn  22287  ustn0  22306  2lgslem1b  25411  2sq  25449  rusgrprc  26780  rgrprcx  26782  wwlksnfi  27123  wlksnwwlknvbijOLD  27126  clwwlkvbij  27390  clwwlkvbijOLD  27391  clwwlkvbijOLDOLD  27392  dfconngr1  27469  isconngr  27470  isconngr1  27471  nmopnegi  29283  nmop0  29304  nmfn0  29305  sa-abvi  29761  abrexdomjm  29797  abrexexd  29799  cbviunf  29824  dfimafnf  29889  ofpreima  29918  cnvoprabOLD  29950  maprnin  29958  fpwrelmapffslem  29959  hasheuni  30597  sigaex  30622  sigaval  30623  isrnsigaOLD  30625  eulerpartlemt  30883  ballotlem2  31001  bnj1146  31313  bnj1400  31357  bnj882  31447  bnj893  31449  derang0  31602  subfaclefac  31609  dfon2lem7  32140  dfon2  32143  domep  32144  dfrdg2  32147  poseq  32200  soseq  32201  madeval2  32383  dfiota3  32477  fvline  32698  ellines  32706  bj-dfifc2  33003  bj-df-ifc  33004  bj-inrab  33354  bj-taginv  33404  bj-nuliotaALT  33450  rnmptsn  33619  dissneqlem  33624  dissneq  33625  dffinxpf  33658  rabiun  33809  ismblfin  33877  volsupnfl  33881  areacirclem5  33930  abrexdom  33951  sdclem1  33964  sdc  33965  rncnvepres  34507  qsresid  34528  rnxrn  34588  rncossdmcoss  34637  psubspset  35703  pmapglb  35729  polval2N  35865  psubclsetN  35895  tendoset  36718  eq0rabdioph  38021  rexrabdioph  38039  eldioph4b  38056  hbtlem6  38379  dfid7  38597  clcnvlem  38608  dfrtrcl5  38614  relopabVD  39792  elabrexg  39861  dffo3f  40014  dfaiota2  41832  dfaimafn2  41917  sprid  42396  setrec2  43114
  Copyright terms: Public domain W3C validator