Theorem abbii 2802

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 2800	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1799	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

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

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 2703

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

This theorem is referenced by:  rabbiiaOLD  3437  rabrab  3455  dfv2  3477  rabab  3502  csb2  3895  cbvcsbw  3903  cbvcsb  3904  csbid  3906  csbcow  3908  csbco  3909  csbconstg  3912  csbie  3929  cbvreucsf  3940  ss2abdv  4060  unabw  4297  notabw  4303  unrab  4305  inrab  4306  inrab2  4307  difrab  4308  rabun2  4313  dfnul4  4324  dfnul2  4325  dfnul3  4326  dfnul2OLD  4327  dfnul3OLD  4328  dfnul4OLD  4329  abf  4402  dfif2  4530  dfsn2ALT  4648  rabsnifsb  4726  tprot  4753  pw0  4815  pwpw0  4816  dfopif  4870  pwsn  4900  pwsnOLD  4901  dfuni2  4910  uniprOLD  4927  dfint2  4952  dfiunv2  5038  cbviun  5039  cbviin  5040  cbviung  5041  cbviing  5042  iunrab  5055  iunidOLD  5064  viin  5068  iunsn  5069  iinuni  5101  cbvopab  5220  cbvopabv  5221  cbvopab1  5223  cbvopab1g  5224  cbvopab2  5225  cbvopab1s  5226  cbvopab1v  5227  cbvopab2v  5229  unopab  5230  zfrep4  5296  zfpair  5419  iunopab  5559  iunopabOLD  5560  dfid2  5576  dfid3  5577  rabxp  5724  csbxp  5775  dfdm3  5887  dfrn2  5888  dfrn3  5889  dfdm4  5895  dfdmf  5896  csbdm  5897  dmun  5910  dmopab  5915  dmopabss  5918  dmopab3  5919  dfrnf  5949  rnopab  5953  rnmpt  5954  dfima2  6061  dfima3  6062  imadmrn  6069  imai  6073  args  6091  mptpreima  6237  dfiota2  6496  cbviotaw  6502  cbviotavw  6503  cbviota  6505  sb8iota  6507  mptfnf  6685  dffv4  6888  dfimafn2  6955  opabiotadm  6973  fndmin  7046  dffo3f  7107  fnasrn  7145  elabrex  7244  abrexco  7245  dfoprab2  7469  cbvoprab2  7499  dmoprab  7512  rnoprab  7514  rnoprab2  7515  fnrnov  7582  abnex  7746  uniuni  7751  zfrep6  7943  fvresex  7948  abrexex2g  7953  abexssex  7959  abexex  7960  oprabrexex2  7967  dfopab2  8040  poseq  8146  soseq  8147  suppvalbr  8152  cnvimadfsn  8159  dfwrecsOLD  8300  dfrecs3  8374  dfrecs3OLD  8375  rdglem1  8417  snec  8776  pmex  8827  fset0  8850  f1setex  8853  0map0sn0  8881  dfixp  8895  cbvixp  8910  pwfir  9178  marypha2lem4  9435  tcsni  9740  scottexs  9884  scott0s  9885  kardex  9891  cardf2  9940  dfac3  10118  infmap2  10215  cf0  10248  cfval2  10257  isf33lem  10363  dffin1-5  10385  axdc2lem  10445  addcompr  11018  mulcompr  11020  dfnn3  12230  hashf1lem2  14421  prprrab  14438  cshwsexa  14778  cshwsexaOLD  14779  trclun  14965  shftdm  15022  hashbc0  16942  lubfval  18307  glbfval  18320  odulub  18364  oduglb  18366  symgbas0  19297  symgsubmefmnd  19307  pmtrprfvalrn  19397  efgval2  19633  dvdsrval  20252  dfrhm2  20365  toponsspwpw  22644  tgval2  22679  tgdif0  22715  xkobval  23310  ustfn  23926  ustn0  23945  2lgslem1b  27119  2sq  27157  madeval2  27573  addsasslem1  27713  addsasslem2  27714  negsid  27742  addsdilem1  27833  addsdilem2  27834  mulsasslem1  27845  mulsasslem2  27846  rusgrprc  29102  rgrprcx  29104  wwlksnfi  29415  clwwlkvbij  29621  dfconngr1  29696  isconngr  29697  isconngr1  29698  nmopnegi  31473  nmop0  31494  nmfn0  31495  sa-abvi  31951  dmrab  31992  abrexdomjm  31999  abrexexd  32001  cbviunf  32042  dfimafnf  32115  ofpreima  32145  intimafv  32187  cnvoprabOLD  32200  maprnin  32211  fpwrelmapffslem  32212  hasheuni  33369  sigaex  33394  sigaval  33395  eulerpartlemt  33656  bnj1146  34088  bnj1400  34132  bnj882  34223  bnj893  34225  dfacycgr1  34421  derang0  34446  subfaclefac  34453  satfdm  34646  fmla0  34659  fmlasuc0  34661  fmla1  34664  dfon2lem7  35053  dfon2  35056  dfrdg2  35059  dfiota3  35187  fvline  35408  ellines  35416  bj-df-ifc  35760  bj-dfif  35761  bj-rababw  36064  bj-inrab  36110  bj-taginv  36170  bj-nuliotaALT  36242  bj-dfid2ALT  36249  rnmptsn  36519  dissneqlem  36524  dissneq  36525  dffinxpf  36569  rabiun  36764  ismblfin  36832  volsupnfl  36836  areacirclem5  36883  abrexdom  36901  sdclem1  36914  sdc  36915  rncnvepres  37475  qsresid  37497  rnxrn  37571  rncossdmcoss  37628  dfcoeleqvrels  37794  mpets  38015  psubspset  38918  pmapglb  38944  polval2N  39080  psubclsetN  39110  tendoset  39933  sticksstones16  41284  sticksstones21  41289  imaopab  41356  prjspeclsp  41656  eq0rabdioph  41816  rexrabdioph  41834  eldioph4b  41851  hbtlem6  42173  onsucrn  42323  dfno2  42481  alephiso2  42611  dfid7  42665  clcnvlem  42676  dfrtrcl5  42682  relopabVD  43964  elabrexg  44030  dfaiota2  46093  dfaimafn2  46173  fundcmpsurinj  46376  fundcmpsurbijinj  46377  sprid  46441  setrec2  47828