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  3407  rabrab  3427  dfv2  3447  rabab  3475  csb2  3861  cbvcsbw  3869  cbvcsb  3870  cbvcsbv  3871  csbid  3872  csbcow  3874  csbco  3875  csbconstg  3878  csbie  3894  cbvreucsf  3903  unabw  4266  notabw  4272  unrab  4274  inrab  4275  inrab2  4276  difrab  4277  rabun2  4283  dfnul4  4294  dfnul2  4295  dfnul3  4296  abf  4365  dfif2  4486  dfsn2ALT  4607  rabsnifsb  4682  tprot  4709  pw0  4772  pwpw0  4773  dfopif  4830  pwsn  4860  dfuni2  4869  dfint2  4908  dfiunv2  4994  cbviun  4995  cbviin  4996  cbviung  4997  cbviing  4998  cbviunv  4999  cbviinv  5000  iunrab  5011  iunidOLD  5020  viin  5024  iunsn  5025  iinuni  5057  cbvopab  5174  cbvopabv  5175  cbvopab1  5176  cbvopab1g  5177  cbvopab2  5178  cbvopab1s  5179  cbvopab1v  5180  cbvopab2v  5181  unopab  5182  zfrep4  5243  zfpair  5371  iunopab  5514  dfid2  5528  dfid3  5529  rabxp  5679  csbxp  5730  dfdm3  5841  dfrn2  5842  dfrn3  5843  dfdm4  5849  dfdmf  5850  csbdm  5851  dmun  5864  dmopab  5869  dmopabss  5872  dmopab3  5873  dfrnf  5903  rnopab  5907  rnopabss  5908  rnopab3  5909  rnmpt  5910  dfima2  6022  dfima3  6023  imadmrn  6030  imai  6034  args  6052  mptpreima  6199  dfiota2  6453  cbviotaw  6459  cbviotavw  6460  cbviota  6461  sb8iota  6463  mptfnf  6635  dffv4  6837  dfimafn2  6906  opabiotadm  6924  fndmin  6999  dffo3f  7060  fnasrn  7099  elabrex  7198  elabrexg  7199  abrexco  7200  dfoprab2  7427  cbvoprab2  7457  cbvoprab12v  7459  cbvoprab3v  7461  dmoprab  7472  rnoprab  7474  rnoprab2  7475  fnrnov  7542  abnex  7713  uniuni  7718  zfrep6  7913  fvresex  7918  abrexex2g  7922  abexssex  7928  abexex  7929  oprabrexex2  7936  dfopab2  8010  poseq  8114  soseq  8115  suppvalbr  8120  cnvimadfsn  8128  dfrecs3  8318  rdglem1  8360  snec  8728  pmex  8781  fset0  8804  f1setex  8807  0map0sn0  8835  dfixp  8849  cbvixp  8864  cbvixpv  8865  pwfir  9242  marypha2lem4  9365  tcsni  9672  scottexs  9816  scott0s  9817  kardex  9823  cardf2  9872  dfac3  10050  infmap2  10146  cf0  10180  cfval2  10189  isf33lem  10295  dffin1-5  10317  axdc2lem  10377  addcompr  10950  mulcompr  10952  dfnn3  12176  hashf1lem2  14397  prprrab  14414  cshwsexa  14765  cshwsexaOLD  14766  trclun  14956  shftdm  15013  hashbc0  16952  lubfval  18289  glbfval  18302  odulub  18346  oduglb  18348  symgbas0  19303  symgsubmefmnd  19312  pmtrprfvalrn  19402  efgval2  19638  dvdsrval  20281  dfrhm2  20394  toponsspwpw  22842  tgval2  22876  tgdif0  22912  xkobval  23506  ustfn  24122  ustn0  24141  2lgslem1b  27336  2sq  27374  madeval2  27798  addsasslem1  27950  addsasslem2  27951  negsid  27987  addsdilem1  28094  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  1p1e2s  28343  twocut  28350  0reno  28401  rusgrprc  29571  rgrprcx  29573  wwlksnfi  29886  clwwlkvbij  30092  dfconngr1  30167  isconngr  30168  isconngr1  30169  nmopnegi  31944  nmop0  31965  nmfn0  31966  sa-abvi  32422  dmrab  32476  abrexdomjm  32486  abrexexd  32488  cbviunf  32534  dfimafnf  32610  ofpreima  32639  intimafv  32684  maprnin  32704  fpwrelmapffslem  32705  hasheuni  34068  sigaex  34093  sigaval  34094  eulerpartlemt  34355  bnj1146  34774  bnj1400  34818  bnj882  34909  bnj893  34911  dfacycgr1  35124  derang0  35149  subfaclefac  35156  satfdm  35349  fmla0  35362  fmlasuc0  35364  fmla1  35367  dfon2lem7  35770  dfon2  35773  dfrdg2  35776  dfiota3  35904  fvline  36125  ellines  36133  sbceqbii  36172  rabeqbii  36175  iuneq12i  36176  iineq1i  36177  iineq12i  36178  ixpeq1i  36181  cbvcsbvw2  36212  cbviunvw2  36213  cbviinvw2  36214  cbvoprab1vw  36218  cbvoprab2vw  36219  cbvoprab123vw  36220  cbvoprab23vw  36221  cbvoprab13vw  36222  cbvixpvw2  36226  bj-df-ifc  36561  bj-dfif  36562  bj-rababw  36862  bj-inrab  36908  bj-taginv  36967  bj-nuliotaALT  37039  bj-dfid2ALT  37046  rnmptsn  37316  dissneqlem  37321  dissneq  37322  dffinxpf  37366  rabiun  37580  ismblfin  37648  volsupnfl  37652  areacirclem5  37699  abrexdom  37717  sdclem1  37730  sdc  37731  rncnvepres  38284  qsresid  38306  dmxrn  38353  dmcnvep  38354  rnxrn  38377  rncossdmcoss  38439  dfcoeleqvrels  38605  mpets  38827  psubspset  39731  pmapglb  39757  polval2N  39893  psubclsetN  39923  tendoset  40746  sticksstones16  42143  sticksstones21  42148  imaopab  42212  prjspeclsp  42593  sn-isghm  42654  eq0rabdioph  42757  rexrabdioph  42775  eldioph4b  42792  hbtlem6  43111  onsucrn  43253  dfno2  43410  alephiso2  43540  dfid7  43594  clcnvlem  43605  dfrtrcl5  43611  relopabVD  44883  iuneq1i  45072  dfaiota2  47080  dfaimafn2  47160  fundcmpsurinj  47403  fundcmpsurbijinj  47404  sprid  47468  stgr1  47953  setrec2  49677