Theorem abbii 2801

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2137, ax-11 2154, and ax-12 2171. (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 2799	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1799	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 205   = wceq 1541  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723

This theorem is referenced by:  rabbiiaOLD  3436  rabrab  3454  dfv2  3476  rabab  3501  csb2  3891  cbvcsbw  3899  cbvcsb  3900  csbid  3902  csbcow  3904  csbco  3905  csbconstg  3908  csbie  3925  cbvreucsf  3936  ss2abdv  4056  unabw  4293  notabw  4299  unrab  4301  inrab  4302  inrab2  4303  difrab  4304  rabun2  4309  dfnul4  4320  dfnul2  4321  dfnul3  4322  dfnul2OLD  4323  dfnul3OLD  4324  dfnul4OLD  4325  abf  4398  dfif2  4524  dfsn2ALT  4642  rabsnifsb  4719  tprot  4746  pw0  4808  pwpw0  4809  dfopif  4863  pwsn  4893  pwsnOLD  4894  dfuni2  4903  uniprOLD  4920  dfint2  4945  dfiunv2  5031  cbviun  5032  cbviin  5033  cbviung  5034  cbviing  5035  iunrab  5048  iunidOLD  5057  viin  5061  iunsn  5062  iinuni  5094  cbvopab  5213  cbvopabv  5214  cbvopab1  5216  cbvopab1g  5217  cbvopab2  5218  cbvopab1s  5219  cbvopab1v  5220  cbvopab2v  5222  unopab  5223  zfrep4  5289  zfpair  5412  iunopab  5552  iunopabOLD  5553  dfid2  5569  dfid3  5570  rabxp  5716  csbxp  5767  dfdm3  5879  dfrn2  5880  dfrn3  5881  dfdm4  5887  dfdmf  5888  csbdm  5889  dmun  5902  dmopab  5907  dmopabss  5910  dmopab3  5911  dfrnf  5941  rnopab  5945  rnmpt  5946  dfima2  6051  dfima3  6052  imadmrn  6059  imai  6062  args  6080  mptpreima  6226  dfiota2  6485  cbviotaw  6491  cbviotavw  6492  cbviota  6494  sb8iota  6496  mptfnf  6672  dffv4  6875  dfimafn2  6942  opabiotadm  6959  fndmin  7031  fnasrn  7127  elabrex  7226  abrexco  7227  dfoprab2  7451  cbvoprab2  7481  dmoprab  7494  rnoprab  7496  rnoprab2  7497  fnrnov  7563  abnex  7727  uniuni  7732  zfrep6  7923  fvresex  7928  abrexex2g  7933  abexssex  7939  abexex  7940  oprabrexex2  7947  dfopab2  8020  poseq  8126  soseq  8127  suppvalbr  8132  cnvimadfsn  8139  dfwrecsOLD  8280  dfrecs3  8354  dfrecs3OLD  8355  rdglem1  8397  snec  8757  pmex  8808  fset0  8831  f1setex  8834  0map0sn0  8862  dfixp  8876  cbvixp  8891  pwfir  9159  marypha2lem4  9415  tcsni  9720  scottexs  9864  scott0s  9865  kardex  9871  cardf2  9920  dfac3  10098  infmap2  10195  cf0  10228  cfval2  10237  isf33lem  10343  dffin1-5  10365  axdc2lem  10425  addcompr  10998  mulcompr  11000  dfnn3  12208  hashf1lem2  14399  prprrab  14416  cshwsexa  14756  cshwsexaOLD  14757  trclun  14943  shftdm  15000  hashbc0  16920  lubfval  18285  glbfval  18298  odulub  18342  oduglb  18344  symgbas0  19220  symgsubmefmnd  19230  pmtrprfvalrn  19320  efgval2  19556  dvdsrval  20127  dfrhm2  20203  toponsspwpw  22353  tgval2  22388  tgdif0  22424  xkobval  23019  ustfn  23635  ustn0  23654  2lgslem1b  26822  2sq  26860  madeval2  27271  addsasslem1  27402  addsasslem2  27403  negsid  27431  addsdilem1  27518  addsdilem2  27519  mulsasslem1  27529  mulsasslem2  27530  rusgrprc  28712  rgrprcx  28714  wwlksnfi  29025  clwwlkvbij  29231  dfconngr1  29306  isconngr  29307  isconngr1  29308  nmopnegi  31081  nmop0  31102  nmfn0  31103  sa-abvi  31559  dmrab  31600  abrexdomjm  31608  abrexexd  31610  cbviunf  31652  dfimafnf  31728  ofpreima  31759  intimafv  31803  cnvoprabOLD  31816  maprnin  31827  fpwrelmapffslem  31828  hasheuni  32912  sigaex  32937  sigaval  32938  eulerpartlemt  33199  bnj1146  33631  bnj1400  33675  bnj882  33766  bnj893  33768  dfacycgr1  33964  derang0  33989  subfaclefac  33996  satfdm  34189  fmla0  34202  fmlasuc0  34204  fmla1  34207  dfon2lem7  34589  dfon2  34592  dfrdg2  34595  dfiota3  34723  fvline  34944  ellines  34952  bj-df-ifc  35259  bj-dfif  35260  bj-rababw  35563  bj-inrab  35609  bj-taginv  35669  bj-nuliotaALT  35741  bj-dfid2ALT  35748  rnmptsn  36018  dissneqlem  36023  dissneq  36024  dffinxpf  36068  rabiun  36263  ismblfin  36331  volsupnfl  36335  areacirclem5  36382  abrexdom  36401  sdclem1  36414  sdc  36415  rncnvepres  36975  qsresid  36997  rnxrn  37071  rncossdmcoss  37128  dfcoeleqvrels  37294  mpets  37515  psubspset  38418  pmapglb  38444  polval2N  38580  psubclsetN  38610  tendoset  39433  sticksstones16  40781  sticksstones21  40786  imaopab  40864  prjspeclsp  41134  eq0rabdioph  41283  rexrabdioph  41301  eldioph4b  41318  hbtlem6  41640  onsucrn  41790  dfno2  41948  alephiso2  42078  dfid7  42132  clcnvlem  42143  dfrtrcl5  42149  relopabVD  43431  elabrexg  43497  dffo3f  43646  dfaiota2  45564  dfaimafn2  45644  fundcmpsurinj  45847  fundcmpsurbijinj  45848  sprid  45912  setrec2  47386