Theorem abbii 2796

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2142, ax-11 2158, and ax-12 2178. (Revised by Steven Nguyen, 3-May-2023.)

Hypothesis

Ref	Expression
abbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
abbii	⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Proof of Theorem abbii

Step	Hyp	Ref	Expression
1		abbi 2794	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1797	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1540  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721

This theorem is referenced by:  rabbiiaOLD  3399  rabrab  3419  dfv2  3439  rabab  3467  csb2  3853  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbid  3864  csbcow  3866  csbco  3867  csbconstg  3870  csbie  3886  cbvreucsf  3895  unabw  4258  notabw  4264  unrab  4266  inrab  4267  inrab2  4268  difrab  4269  rabun2  4275  dfnul4  4286  dfnul2  4287  dfnul3  4288  abf  4357  dfif2  4478  dfsn2ALT  4599  rabsnifsb  4674  tprot  4701  pw0  4763  pwpw0  4764  dfopif  4821  pwsn  4851  dfuni2  4860  dfint2  4898  dfiunv2  4984  cbviun  4985  cbviin  4986  cbviung  4987  cbviing  4988  cbviunv  4989  cbviinv  4990  iunrab  5001  iunidOLD  5010  viin  5014  iunsn  5015  iinuni  5047  cbvopab  5164  cbvopabv  5165  cbvopab1  5166  cbvopab1g  5167  cbvopab2  5168  cbvopab1s  5169  cbvopab1v  5170  cbvopab2v  5171  unopab  5172  zfrep4  5232  zfpair  5360  iunopab  5502  dfid2  5516  dfid3  5517  rabxp  5667  csbxp  5719  dfdm3  5830  dfrn2  5831  dfrn3  5832  dfdm4  5838  dfdmf  5839  csbdm  5840  dmun  5853  dmopab  5858  dmopabss  5861  dmopab3  5862  dfrnf  5892  rnopab  5896  rnopabss  5897  rnopab3  5898  rnmpt  5899  dfima2  6013  dfima3  6014  imadmrn  6021  imai  6025  args  6043  mptpreima  6187  dfiota2  6439  cbviotaw  6445  cbviotavw  6446  cbviota  6447  sb8iota  6449  mptfnf  6617  dffv4  6819  dfimafn2  6886  opabiotadm  6904  fndmin  6979  dffo3f  7040  fnasrn  7079  elabrex  7178  elabrexg  7179  abrexco  7180  dfoprab2  7407  cbvoprab2  7437  cbvoprab12v  7439  cbvoprab3v  7441  dmoprab  7452  rnoprab  7454  rnoprab2  7455  fnrnov  7522  abnex  7693  uniuni  7698  zfrep6  7890  fvresex  7895  abrexex2g  7899  abexssex  7905  abexex  7906  oprabrexex2  7913  dfopab2  7987  poseq  8091  soseq  8092  suppvalbr  8097  cnvimadfsn  8105  dfrecs3  8295  rdglem1  8337  snec  8705  pmex  8758  fset0  8781  f1setex  8784  0map0sn0  8812  dfixp  8826  cbvixp  8841  cbvixpv  8842  pwfir  9206  marypha2lem4  9328  tcsni  9639  scottexs  9783  scott0s  9784  kardex  9790  cardf2  9839  dfac3  10015  infmap2  10111  cf0  10145  cfval2  10154  isf33lem  10260  dffin1-5  10282  axdc2lem  10342  addcompr  10915  mulcompr  10917  dfnn3  12142  hashf1lem2  14363  prprrab  14380  cshwsexa  14730  cshwsexaOLD  14731  trclun  14921  shftdm  14978  hashbc0  16917  lubfval  18254  glbfval  18267  odulub  18311  oduglb  18313  symgbas0  19268  symgsubmefmnd  19277  pmtrprfvalrn  19367  efgval2  19603  dvdsrval  20246  dfrhm2  20359  toponsspwpw  22807  tgval2  22841  tgdif0  22877  xkobval  23471  ustfn  24087  ustn0  24106  2lgslem1b  27301  2sq  27339  madeval2  27763  addsasslem1  27915  addsasslem2  27916  negsid  27952  addsdilem1  28059  addsdilem2  28060  mulsasslem1  28071  mulsasslem2  28072  1p1e2s  28308  twocut  28315  0reno  28366  rusgrprc  29536  rgrprcx  29538  wwlksnfi  29851  clwwlkvbij  30057  dfconngr1  30132  isconngr  30133  isconngr1  30134  nmopnegi  31909  nmop0  31930  nmfn0  31931  sa-abvi  32387  dmrab  32441  abrexdomjm  32451  abrexexd  32453  cbviunf  32499  dfimafnf  32579  ofpreima  32608  intimafv  32653  maprnin  32674  fpwrelmapffslem  32675  hasheuni  34052  sigaex  34077  sigaval  34078  eulerpartlemt  34339  bnj1146  34758  bnj1400  34802  bnj882  34893  bnj893  34895  dfacycgr1  35117  derang0  35142  subfaclefac  35149  satfdm  35342  fmla0  35355  fmlasuc0  35357  fmla1  35360  dfon2lem7  35763  dfon2  35766  dfrdg2  35769  dfiota3  35897  fvline  36118  ellines  36126  sbceqbii  36165  rabeqbii  36168  iuneq12i  36169  iineq1i  36170  iineq12i  36171  ixpeq1i  36174  cbvcsbvw2  36205  cbviunvw2  36206  cbviinvw2  36207  cbvoprab1vw  36211  cbvoprab2vw  36212  cbvoprab123vw  36213  cbvoprab23vw  36214  cbvoprab13vw  36215  cbvixpvw2  36219  bj-df-ifc  36554  bj-dfif  36555  bj-rababw  36855  bj-inrab  36901  bj-taginv  36960  bj-nuliotaALT  37032  bj-dfid2ALT  37039  rnmptsn  37309  dissneqlem  37314  dissneq  37315  dffinxpf  37359  rabiun  37573  ismblfin  37641  volsupnfl  37645  areacirclem5  37692  abrexdom  37710  sdclem1  37723  sdc  37724  rncnvepres  38277  qsresid  38299  dmxrn  38346  dmcnvep  38347  rnxrn  38370  rncossdmcoss  38432  dfcoeleqvrels  38598  mpets  38820  psubspset  39723  pmapglb  39749  polval2N  39885  psubclsetN  39915  tendoset  40738  sticksstones16  42135  sticksstones21  42140  imaopab  42204  prjspeclsp  42585  sn-isghm  42646  eq0rabdioph  42749  rexrabdioph  42767  eldioph4b  42784  hbtlem6  43102  onsucrn  43244  dfno2  43401  alephiso2  43531  dfid7  43585  clcnvlem  43596  dfrtrcl5  43602  relopabVD  44874  iuneq1i  45063  dfaiota2  47070  dfaimafn2  47150  fundcmpsurinj  47393  fundcmpsurbijinj  47394  sprid  47458  stgr1  47945  setrec2  49680