Theorem abbii 2803

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

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

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 2708

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

This theorem is referenced by:  rabbiiaOLD  3425  rabrab  3445  dfv2  3467  rabab  3496  csb2  3881  cbvcsbw  3889  cbvcsb  3890  cbvcsbv  3891  csbid  3892  csbcow  3894  csbco  3895  csbconstg  3898  csbie  3914  cbvreucsf  3923  unabw  4287  notabw  4293  unrab  4295  inrab  4296  inrab2  4297  difrab  4298  rabun2  4304  dfnul4  4315  dfnul2  4316  dfnul3  4317  abf  4386  dfif2  4507  dfsn2ALT  4628  rabsnifsb  4703  tprot  4730  pw0  4793  pwpw0  4794  dfopif  4851  pwsn  4881  dfuni2  4890  dfint2  4929  dfiunv2  5016  cbviun  5017  cbviin  5018  cbviung  5019  cbviing  5020  cbviunv  5021  cbviinv  5022  iunrab  5033  iunidOLD  5042  viin  5046  iunsn  5047  iinuni  5079  cbvopab  5196  cbvopabv  5197  cbvopab1  5198  cbvopab1g  5199  cbvopab2  5200  cbvopab1s  5201  cbvopab1v  5202  cbvopab2v  5204  unopab  5205  zfrep4  5268  zfpair  5396  iunopab  5539  iunopabOLD  5540  dfid2  5555  dfid3  5556  rabxp  5707  csbxp  5759  dfdm3  5872  dfrn2  5873  dfrn3  5874  dfdm4  5880  dfdmf  5881  csbdm  5882  dmun  5895  dmopab  5900  dmopabss  5903  dmopab3  5904  dfrnf  5935  rnopab  5939  rnopabss  5940  rnopab3  5941  rnmpt  5942  dfima2  6054  dfima3  6055  imadmrn  6062  imai  6066  args  6084  mptpreima  6232  dfiota2  6490  cbviotaw  6496  cbviotavw  6497  cbviota  6498  sb8iota  6500  mptfnf  6678  dffv4  6878  dfimafn2  6947  opabiotadm  6965  fndmin  7040  dffo3f  7101  fnasrn  7140  elabrex  7239  elabrexg  7240  abrexco  7241  dfoprab2  7470  cbvoprab2  7500  cbvoprab12v  7502  cbvoprab3v  7504  dmoprab  7515  rnoprab  7517  rnoprab2  7518  fnrnov  7585  abnex  7756  uniuni  7761  zfrep6  7958  fvresex  7963  abrexex2g  7968  abexssex  7974  abexex  7975  oprabrexex2  7982  dfopab2  8056  poseq  8162  soseq  8163  suppvalbr  8168  cnvimadfsn  8176  dfwrecsOLD  8317  dfrecs3  8391  dfrecs3OLD  8392  rdglem1  8434  snec  8799  pmex  8850  fset0  8873  f1setex  8876  0map0sn0  8904  dfixp  8918  cbvixp  8933  cbvixpv  8934  pwfir  9332  marypha2lem4  9455  tcsni  9762  scottexs  9906  scott0s  9907  kardex  9913  cardf2  9962  dfac3  10140  infmap2  10236  cf0  10270  cfval2  10279  isf33lem  10385  dffin1-5  10407  axdc2lem  10467  addcompr  11040  mulcompr  11042  dfnn3  12259  hashf1lem2  14479  prprrab  14496  cshwsexa  14847  cshwsexaOLD  14848  trclun  15038  shftdm  15095  hashbc0  17030  lubfval  18365  glbfval  18378  odulub  18422  oduglb  18424  symgbas0  19375  symgsubmefmnd  19384  pmtrprfvalrn  19474  efgval2  19710  dvdsrval  20326  dfrhm2  20439  toponsspwpw  22865  tgval2  22899  tgdif0  22935  xkobval  23529  ustfn  24145  ustn0  24164  2lgslem1b  27360  2sq  27398  madeval2  27818  addsasslem1  27967  addsasslem2  27968  negsid  28004  addsdilem1  28111  addsdilem2  28112  mulsasslem1  28123  mulsasslem2  28124  1p1e2s  28359  twocut  28366  0reno  28405  rusgrprc  29575  rgrprcx  29577  wwlksnfi  29893  clwwlkvbij  30099  dfconngr1  30174  isconngr  30175  isconngr1  30176  nmopnegi  31951  nmop0  31972  nmfn0  31973  sa-abvi  32429  dmrab  32483  abrexdomjm  32493  abrexexd  32495  cbviunf  32541  dfimafnf  32619  ofpreima  32648  intimafv  32693  maprnin  32713  fpwrelmapffslem  32714  hasheuni  34121  sigaex  34146  sigaval  34147  eulerpartlemt  34408  bnj1146  34827  bnj1400  34871  bnj882  34962  bnj893  34964  dfacycgr1  35171  derang0  35196  subfaclefac  35203  satfdm  35396  fmla0  35409  fmlasuc0  35411  fmla1  35414  dfon2lem7  35812  dfon2  35815  dfrdg2  35818  dfiota3  35946  fvline  36167  ellines  36175  sbceqbii  36214  rabeqbii  36217  iuneq12i  36218  iineq1i  36219  iineq12i  36220  ixpeq1i  36223  cbvcsbvw2  36254  cbviunvw2  36255  cbviinvw2  36256  cbvoprab1vw  36260  cbvoprab2vw  36261  cbvoprab123vw  36262  cbvoprab23vw  36263  cbvoprab13vw  36264  cbvixpvw2  36268  bj-df-ifc  36603  bj-dfif  36604  bj-rababw  36904  bj-inrab  36950  bj-taginv  37009  bj-nuliotaALT  37081  bj-dfid2ALT  37088  rnmptsn  37358  dissneqlem  37363  dissneq  37364  dffinxpf  37408  rabiun  37622  ismblfin  37690  volsupnfl  37694  areacirclem5  37741  abrexdom  37759  sdclem1  37772  sdc  37773  rncnvepres  38326  qsresid  38348  rnxrn  38421  rncossdmcoss  38478  dfcoeleqvrels  38644  mpets  38865  psubspset  39768  pmapglb  39794  polval2N  39930  psubclsetN  39960  tendoset  40783  sticksstones16  42180  sticksstones21  42185  imaopab  42249  prjspeclsp  42610  sn-isghm  42671  eq0rabdioph  42774  rexrabdioph  42792  eldioph4b  42809  hbtlem6  43128  onsucrn  43270  dfno2  43427  alephiso2  43557  dfid7  43611  clcnvlem  43622  dfrtrcl5  43628  relopabVD  44900  iuneq1i  45089  dfaiota2  47095  dfaimafn2  47175  fundcmpsurinj  47403  fundcmpsurbijinj  47404  sprid  47468  stgr1  47953  setrec2  49539