Theorem abbii 2830

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

Syntax hints:   ↔ wb 209   = wceq 1570  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755

This theorem is referenced by:  dfv2  3458  rabab  3485  csb2  3855  cbvcsbw  3863  cbvcsb  3864  cbvcsbv  3865  csbid  3866  csbcow  3868  csbco  3869  csbconstg  3872  csbie  3888  cbvreucsf  3897  unabw  4260  notabw  4266  unrab  4268  inrab  4269  inrab2  4270  difrab  4271  rabun2  4277  dfnul4  4288  dfnul2  4289  dfnul3  4290  abf  4371  dfif2  4489  dfsn2ALT  4611  rabsnifsb  4688  tprot  4715  pw0  4778  pwpw0  4779  dfopif  4835  pwsn  4865  dfuni2  4874  dfint2  4914  dfiunv2  4998  cbviun  4999  cbviin  5000  cbviung  5001  cbviing  5002  cbviunv  5003  cbviinv  5004  iunrab  5017  viin  5029  iunsn  5030  iinuni  5064  cbvopab  5183  cbvopabv  5184  cbvopab1  5185  cbvopab1g  5186  cbvopab2  5187  cbvopab1s  5188  cbvopab1v  5189  cbvopab2v  5190  unopab  5191  zfrep4  5254  zfpair  5392  iunopab  5544  dfid2  5558  dfid3  5559  rabxp  5709  csbxp  5762  dfdm3  5877  dfrn2  5878  dfrn3  5879  dfdm4  5885  dfdmf  5886  csbdm  5887  dmun  5900  dmopab  5905  dmopabss  5908  dmopab3  5909  dfrnf  5940  rnopab  5944  rnopabss  5945  rnopab3  5946  rnmpt  5947  dfima2  6064  dfima3  6065  imadmrn  6072  imai  6076  args  6094  mptpreima  6239  dfiota2  6493  cbviotaw  6499  cbviotavw  6500  cbviota  6501  sb8iota  6503  mptfnf  6670  dffv4  6878  dfimafn2  6944  opabiotadm  6962  fndmin  7040  dffo3f  7101  fnasrn  7141  elabrex  7240  elabrexg  7241  abrexco  7242  dfoprab2  7468  cbvoprab2  7498  cbvoprab12v  7500  cbvoprab3v  7502  dmoprab  7513  rnoprab  7515  rnoprab2  7516  fnrnov  7583  abnex  7752  uniuni  7757  zfrep6OLD  7948  fvresex  7953  abrexex2g  7957  abexssex  7963  abexex  7964  oprabrexex2  7971  dfopab2  8045  poseq  8150  soseq  8151  suppvalbr  8156  cnvimadfsn  8164  dfrecs3  8355  rdglem1  8398  snec  8772  pmex  8825  fset0  8847  f1setex  8850  0map0sn0  8879  dfixp  8893  cbvixp  8908  cbvixpv  8909  pwfir  9272  marypha2lem4  9394  tcsni  9706  scottexs  9857  scott0s  9858  kardex  9876  cardf2  9925  dfac3  10101  infmap2  10196  cf0  10229  cfval2  10239  isf33lem  10345  dffin1-5  10367  axdc2lem  10427  addcompr  11001  mulcompr  11003  dfnn3  12242  hashf1lem2  14489  prprrab  14506  cshwsexa  14857  trclun  15047  shftdm  15104  hashbc0  17060  lubfval  18399  glbfval  18412  odulub  18456  oduglb  18458  symgbas0  19454  symgsubmefmnd  19463  pmtrprfvalrn  19553  efgval2  19789  dvdsrval  20439  dfrhm2  20552  toponsspwpw  23079  tgval2  23113  tgdif0  23149  xkobval  23743  ustfn  24359  ustn0  24378  2lgslem1b  27556  2sq  27594  madeval2  28026  addsasslem1  28196  addsasslem2  28197  negsid  28234  addsdilem1  28344  addsdilem2  28345  mulsasslem1  28356  mulsasslem2  28357  twocut  28616  pw2cut2  28655  rusgrprc  29940  rgrprcx  29942  wwlksnfi  30255  clwwlkvbij  30464  dfconngr1  30539  isconngr  30540  isconngr1  30541  nmopnegi  32317  nmop0  32338  nmfn0  32339  sa-abvi  32795  dmrab  32843  abrexdomjm  32853  abrexexd  32855  cbviunf  32900  dfimafnf  32981  ofpreima  33010  intimafv  33056  maprnin  33076  fpwrelmapffslem  33077  hasheuni  34475  sigaex  34500  sigaval  34501  eulerpartlemt  34761  bnj1146  35179  bnj1400  35223  bnj882  35314  bnj893  35316  dfacycgr1  35636  derang0  35661  subfaclefac  35668  satfdm  35861  fmla0  35874  fmlasuc0  35876  fmla1  35879  dfon2lem7  36279  dfon2  36282  dfrdg2  36285  dfiota3  36413  fvline  36636  ellines  36644  sbceqbii  36703  rabeqbii  36706  iuneq12i  36707  iineq1i  36708  iineq12i  36709  ixpeq1i  36712  cbvcsbvw2  36743  cbviunvw2  36744  cbviinvw2  36745  cbvoprab1vw  36749  cbvoprab2vw  36750  cbvoprab123vw  36751  cbvoprab23vw  36752  cbvoprab13vw  36753  cbvixpvw2  36757  bj-dfnul2  37163  bj-df-ifc  37173  bj-dfif  37174  bj-rababw  37516  bj-inrab  37563  bj-taginv  37622  bj-nuliotaALT  37694  bj-dfid2ALT  37701  rnmptsn  37981  dissneqlem  37986  dissneq  37987  dffinxpf  38031  rabiun  38244  ismblfin  38312  volsupnfl  38316  areacirclem5  38363  abrexdom  38381  sdclem1  38394  sdc  38395  rncnvepres  38958  qsresid  38980  dmxrn  39036  dmcnvep  39037  rnxrn  39070  dfsuccl3  39122  dfsuccl4  39123  rncossdmcoss  39194  dfcoeleqvrels  39354  mpets  39605  psubspset  40518  pmapglb  40544  polval2N  40680  psubclsetN  40710  tendoset  41533  sticksstones16  42929  sticksstones21  42934  imaopab  43002  prjspeclsp  43344  sn-isghm  43405  eq0rabdioph  43507  rexrabdioph  43521  eldioph4b  43538  hbtlem6  43856  onsucrn  43998  dfno2  44154  alephiso2  44284  dfid7  44338  clcnvlem  44349  dfrtrcl5  44355  relopabVD  45609  iuneq1i  45804  dfaiota2  47823  dfaimafn2  47903  fundcmpsurinj  48158  fundcmpsurbijinj  48159  sprid  48223  stgr1  48726  setrec2  50473