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

Theorem abbii 2722
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 2720 . 2 (∀𝑥(𝜑𝜓) ↔ {𝑥𝜑} = {𝑥𝜓})
2 abbii.1 . 2 (𝜑𝜓)
31, 2mpgbi 1715 1 {𝑥𝜑} = {𝑥𝜓}
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  {cab 2592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602
This theorem is referenced by:  rabswap  3094  rabbiia  3157  rabab  3192  csb2  3497  cbvcsb  3500  csbid  3503  csbco  3505  cbvreucsf  3529  unrab  3853  inrab  3854  inrab2  3855  difrab  3856  rabun2  3861  dfnul3  3873  rab0OLD  3906  dfif2  4034  rabsnifsb  4197  tprot  4224  pw0  4279  pwpw0  4280  dfopif  4328  pwsn  4357  pwsnALT  4358  dfuni2  4365  unipr  4376  dfint2  4403  int0OLD  4417  rabasiun  4450  dfiunv2  4483  cbviun  4484  cbviin  4485  iunrab  4494  iunid  4502  viin  4506  iinuni  4536  cbvopab  4644  cbvopab1  4646  cbvopab2  4647  cbvopab1s  4648  cbvopab2v  4650  unopab  4651  zfrep4  4698  zfpair  4823  iunopab  4923  dfid3  4941  rabxp  5065  csbxp  5110  dfdm3  5217  dfrn2  5218  dfrn3  5219  dfdm4  5222  dfdmf  5223  csbdm  5224  dmun  5237  dmopab  5241  dmopabss  5242  dmopab3  5243  dfrnf  5269  rnopab  5275  rnmpt  5276  dfima2  5371  dfima3  5372  imadmrn  5379  imai  5381  args  5396  mptpreima  5528  dfiota2  5752  cbviota  5756  sb8iota  5758  mptfnf  5911  dffv4  6082  dfimafn2  6138  opabiotadm  6152  fndmin  6214  fnasrn  6299  elabrex  6380  abrexco  6381  dfoprab2  6574  cbvoprab2  6601  dmoprab  6614  rnoprab  6616  rnoprab2  6617  fnrnov  6679  uniuni  6839  zfrep6  7001  fvresex  7006  abrexex2g  7010  abrexex2  7014  abexssex  7015  abexex  7016  oprabrexex2  7023  dfopab2  7087  suppvalbr  7160  cnvimadfsn  7165  dfrecs3  7330  rdglem1  7372  snec  7671  pmex  7723  dfixp  7770  cbvixp  7785  marypha2lem4  8201  ruv  8364  tcsni  8476  scottexs  8607  scott0s  8608  kardex  8614  cardf2  8626  dfac3  8801  infmap2  8897  cf0  8930  cfval2  8939  isf33lem  9045  dffin1-5  9067  axdc2lem  9127  addcompr  9696  mulcompr  9698  dfnn3  10878  hashf1lem2  13046  cshwsexa  13364  trclun  13546  shftdm  13602  hashbc0  15490  lubfval  16744  glbfval  16757  oduglb  16905  odulub  16907  symgbas0  17580  pmtrprfvalrn  17674  efgval2  17903  dvdsrval  18411  dfrhm2  18483  tgval2  20510  tgdif0  20546  xkobval  21138  ustfn  21754  ustn0  21773  2lgslem1b  24831  2sq  24869  usgraop  25642  wwlknprop  25977  wwlknfi  26029  wlknwwlknvbij  26031  clwwlkvbij  26092  vdgrun  26191  vdgrfiun  26192  nmopnegi  28011  nmop0  28032  nmfn0  28033  foo3  28489  rabrab  28525  abrexdomjm  28532  abrexexd  28534  cbviunf  28558  dfimafnf  28620  ofpreima  28651  cnvoprab  28689  maprnin  28697  fpwrelmapffslem  28698  hasheuni  29277  sigaex  29302  sigaval  29303  isrnsigaOLD  29305  eulerpartlemt  29563  ballotlem2  29680  bnj1146  29919  bnj1400  29963  bnj882  30053  bnj893  30055  derang0  30208  subfaclefac  30215  dfon2lem7  30741  dfon2  30744  domep  30745  dfrdg2  30748  poseq  30797  soseq  30798  dfiota3  31003  fvline  31224  ellines  31232  bj-dfifc2  31537  bj-df-ifc  31538  bj-inrab  31915  bj-taginv  31967  bj-nuliotaALT  32011  bj-toponss  32041  rnmptsn  32158  dissneqlem  32163  dissneq  32164  dffinxpf  32198  rabiun  32352  ismblfin  32420  volsupnfl  32424  areacirclem5  32474  abrexdom  32495  sdclem1  32509  sdc  32510  psubspset  33848  pmapglb  33874  polval2N  34010  psubclsetN  34040  tendoset  34865  eq0rabdioph  36158  rexrabdioph  36176  eldioph4b  36193  hbtlem6  36518  dfid7  36738  clcnvlem  36749  dfrtrcl5  36755  relopabVD  37959  elabrexg  38029  dffo3f  38159  dfaimafn2  39697  prprrab  40194  rusgrprc  40789  rgrprcx  40791  wwlksnfi  41111  wlksnwwlknvbij  41113  clwwlksvbij  41228  dfconngr1  41354  isconngr  41355  isconngr1  41356
  Copyright terms: Public domain W3C validator