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

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

Proof of Theorem abbii
StepHypRef Expression
1 abbi 2734 . 2 (∀𝑥(𝜑𝜓) ↔ {𝑥𝜑} = {𝑥𝜓})
2 abbii.1 . 2 (𝜑𝜓)
31, 2mpgbi 1722 1 {𝑥𝜑} = {𝑥𝜓}
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1480  {cab 2607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617
This theorem is referenced by:  rabswap  3114  rabbiia  3177  rabab  3213  csb2  3521  cbvcsb  3524  csbid  3527  csbco  3529  cbvreucsf  3553  unrab  3880  inrab  3881  inrab2  3882  difrab  3883  rabun2  3888  dfnul3  3900  rab0OLD  3936  dfif2  4066  rabsnifsb  4234  tprot  4261  pw0  4318  pwpw0  4319  dfopif  4374  pwsn  4403  pwsnALT  4404  dfuni2  4411  unipr  4422  dfint2  4449  int0OLD  4463  rabasiun  4496  dfiunv2  4529  cbviun  4530  cbviin  4531  iunrab  4540  iunid  4548  viin  4552  iinuni  4582  cbvopab  4693  cbvopab1  4695  cbvopab2  4696  cbvopab1s  4697  cbvopab2v  4699  unopab  4700  zfrep4  4749  zfpair  4875  iunopab  4982  dfid3  5000  rabxp  5124  csbxp  5171  dfdm3  5280  dfrn2  5281  dfrn3  5282  dfdm4  5286  dfdmf  5287  csbdm  5288  dmun  5301  dmopab  5305  dmopabss  5306  dmopab3  5307  dfrnf  5334  rnopab  5340  rnmpt  5341  dfima2  5437  dfima3  5438  imadmrn  5445  imai  5447  args  5462  mptpreima  5597  dfiota2  5821  cbviota  5825  sb8iota  5827  mptfnf  5982  dffv4  6155  dfimafn2  6213  opabiotadm  6227  fndmin  6290  fnasrn  6376  elabrex  6466  abrexco  6467  dfoprab2  6666  cbvoprab2  6693  dmoprab  6706  rnoprab  6708  rnoprab2  6709  fnrnov  6772  uniuni  6935  zfrep6  7096  fvresex  7101  abrexex2g  7105  abrexex2  7109  abexssex  7110  abexex  7111  oprabrexex2  7118  dfopab2  7182  suppvalbr  7259  cnvimadfsn  7264  dfrecs3  7429  rdglem1  7471  snec  7770  pmex  7822  dfixp  7870  cbvixp  7885  marypha2lem4  8304  ruv  8467  tcsni  8579  scottexs  8710  scott0s  8711  kardex  8717  cardf2  8729  dfac3  8904  infmap2  9000  cf0  9033  cfval2  9042  isf33lem  9148  dffin1-5  9170  axdc2lem  9230  addcompr  9803  mulcompr  9805  dfnn3  10994  hashf1lem2  13194  prprrab  13209  cshwsexa  13523  trclun  13705  shftdm  13761  hashbc0  15652  lubfval  16918  glbfval  16931  oduglb  17079  odulub  17081  symgbas0  17754  pmtrprfvalrn  17848  efgval2  18077  dvdsrval  18585  dfrhm2  18657  toponsspwpw  20666  tgval2  20700  tgdif0  20736  xkobval  21329  ustfn  21945  ustn0  21964  2lgslem1b  25051  2sq  25089  rusgrprc  26390  rgrprcx  26392  wwlksnfi  26704  wlksnwwlknvbij  26706  clwwlksvbij  26822  dfconngr1  26948  isconngr  26949  isconngr1  26950  nmopnegi  28712  nmop0  28733  nmfn0  28734  foo3  29190  rabrab  29227  abrexdomjm  29233  abrexexd  29235  cbviunf  29259  dfimafnf  29320  ofpreima  29349  cnvoprab  29382  maprnin  29390  fpwrelmapffslem  29391  hasheuni  29970  sigaex  29995  sigaval  29996  isrnsigaOLD  29998  eulerpartlemt  30256  ballotlem2  30373  bnj1146  30623  bnj1400  30667  bnj882  30757  bnj893  30759  derang0  30912  subfaclefac  30919  dfon2lem7  31448  dfon2  31451  domep  31452  dfrdg2  31455  poseq  31504  soseq  31505  dfiota3  31725  fvline  31946  ellines  31954  bj-dfifc2  32259  bj-df-ifc  32260  bj-inrab  32623  bj-taginv  32674  bj-nuliotaALT  32720  rnmptsn  32853  dissneqlem  32858  dissneq  32859  dffinxpf  32893  rabiun  33053  ismblfin  33121  volsupnfl  33125  areacirclem5  33175  abrexdom  33196  sdclem1  33210  sdc  33211  psubspset  34549  pmapglb  34575  polval2N  34711  psubclsetN  34741  tendoset  35566  eq0rabdioph  36859  rexrabdioph  36877  eldioph4b  36894  hbtlem6  37219  dfid7  37439  clcnvlem  37450  dfrtrcl5  37456  relopabVD  38659  elabrexg  38728  dffo3f  38873  dfaimafn2  40580  sprid  41042  setrec2  41765
  Copyright terms: Public domain W3C validator