Theorem abbii 2803

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2147, ax-11 2163, and ax-12 2185. (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 1799	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

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

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  dfv2  3432  rabab  3460  csb2  3839  cbvcsbw  3847  cbvcsb  3848  cbvcsbv  3849  csbid  3850  csbcow  3852  csbco  3853  csbconstg  3856  csbie  3872  cbvreucsf  3881  unabw  4247  notabw  4253  unrab  4255  inrab  4256  inrab2  4257  difrab  4258  rabun2  4264  dfnul4  4275  dfnul2  4276  dfnul3  4277  abf  4346  dfif2  4468  dfsn2ALT  4589  rabsnifsb  4666  tprot  4693  pw0  4755  pwpw0  4756  dfopif  4813  pwsn  4843  dfuni2  4852  dfint2  4891  dfiunv2  4976  cbviun  4977  cbviin  4978  cbviung  4979  cbviing  4980  cbviunv  4981  cbviinv  4982  iunrab  4995  viin  5007  iunsn  5008  iinuni  5040  cbvopab  5157  cbvopabv  5158  cbvopab1  5159  cbvopab1g  5160  cbvopab2  5161  cbvopab1s  5162  cbvopab1v  5163  cbvopab2v  5164  unopab  5165  zfrep4  5228  zfpair  5363  iunopab  5514  dfid2  5528  dfid3  5529  rabxp  5679  csbxp  5732  dfdm3  5842  dfrn2  5843  dfrn3  5844  dfdm4  5850  dfdmf  5851  csbdm  5852  dmun  5865  dmopab  5870  dmopabss  5873  dmopab3  5874  dfrnf  5905  rnopab  5909  rnopabss  5910  rnopab3  5911  rnmpt  5912  dfima2  6027  dfima3  6028  imadmrn  6035  imai  6039  args  6057  mptpreima  6202  dfiota2  6455  cbviotaw  6461  cbviotavw  6462  cbviota  6463  sb8iota  6465  mptfnf  6633  dffv4  6837  dfimafn2  6903  opabiotadm  6921  fndmin  6997  dffo3f  7058  fnasrn  7098  elabrex  7197  elabrexg  7198  abrexco  7199  dfoprab2  7425  cbvoprab2  7455  cbvoprab12v  7457  cbvoprab3v  7459  dmoprab  7470  rnoprab  7472  rnoprab2  7473  fnrnov  7540  abnex  7711  uniuni  7716  zfrep6OLD  7908  fvresex  7913  abrexex2g  7917  abexssex  7923  abexex  7924  oprabrexex2  7931  dfopab2  8005  poseq  8108  soseq  8109  suppvalbr  8114  cnvimadfsn  8122  dfrecs3  8312  rdglem1  8354  snec  8725  pmex  8778  fset0  8801  f1setex  8804  0map0sn0  8833  dfixp  8847  cbvixp  8862  cbvixpv  8863  pwfir  9227  marypha2lem4  9351  tcsni  9662  scottexs  9811  scott0s  9812  kardex  9818  cardf2  9867  dfac3  10043  infmap2  10139  cf0  10173  cfval2  10182  isf33lem  10288  dffin1-5  10310  axdc2lem  10370  addcompr  10944  mulcompr  10946  dfnn3  12188  hashf1lem2  14418  prprrab  14435  cshwsexa  14786  trclun  14976  shftdm  15033  hashbc0  16976  lubfval  18314  glbfval  18327  odulub  18371  oduglb  18373  symgbas0  19364  symgsubmefmnd  19373  pmtrprfvalrn  19463  efgval2  19699  dvdsrval  20341  dfrhm2  20454  toponsspwpw  22887  tgval2  22921  tgdif0  22957  xkobval  23551  ustfn  24167  ustn0  24186  2lgslem1b  27355  2sq  27393  madeval2  27825  addsasslem1  27995  addsasslem2  27996  negsid  28033  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  twocut  28415  pw2cut2  28454  rusgrprc  29659  rgrprcx  29661  wwlksnfi  29974  clwwlkvbij  30183  dfconngr1  30258  isconngr  30259  isconngr1  30260  nmopnegi  32036  nmop0  32057  nmfn0  32058  sa-abvi  32514  dmrab  32566  abrexdomjm  32577  abrexexd  32579  cbviunf  32625  dfimafnf  32709  ofpreima  32738  intimafv  32784  maprnin  32804  fpwrelmapffslem  32805  hasheuni  34229  sigaex  34254  sigaval  34255  eulerpartlemt  34515  bnj1146  34933  bnj1400  34977  bnj882  35068  bnj893  35070  dfacycgr1  35326  derang0  35351  subfaclefac  35358  satfdm  35551  fmla0  35564  fmlasuc0  35566  fmla1  35569  dfon2lem7  35969  dfon2  35972  dfrdg2  35975  dfiota3  36103  fvline  36326  ellines  36334  sbceqbii  36373  rabeqbii  36376  iuneq12i  36377  iineq1i  36378  iineq12i  36379  ixpeq1i  36382  cbvcsbvw2  36413  cbviunvw2  36414  cbviinvw2  36415  cbvoprab1vw  36419  cbvoprab2vw  36420  cbvoprab123vw  36421  cbvoprab23vw  36422  cbvoprab13vw  36423  cbvixpvw2  36427  bj-dfnul2  36835  bj-df-ifc  36845  bj-dfif  36846  bj-rababw  37188  bj-inrab  37234  bj-taginv  37293  bj-nuliotaALT  37365  bj-dfid2ALT  37372  rnmptsn  37651  dissneqlem  37656  dissneq  37657  dffinxpf  37701  rabiun  37914  ismblfin  37982  volsupnfl  37986  areacirclem5  38033  abrexdom  38051  sdclem1  38064  sdc  38065  rncnvepres  38630  qsresid  38652  dmxrn  38708  dmcnvep  38709  rnxrn  38742  dfsuccl3  38794  dfsuccl4  38795  rncossdmcoss  38866  dfcoeleqvrels  39026  mpets  39277  psubspset  40190  pmapglb  40216  polval2N  40352  psubclsetN  40382  tendoset  41205  sticksstones16  42601  sticksstones21  42606  imaopab  42672  prjspeclsp  43045  sn-isghm  43106  eq0rabdioph  43208  rexrabdioph  43222  eldioph4b  43239  hbtlem6  43557  onsucrn  43699  dfno2  43855  alephiso2  43985  dfid7  44039  clcnvlem  44050  dfrtrcl5  44056  relopabVD  45327  iuneq1i  45515  dfaiota2  47534  dfaimafn2  47614  fundcmpsurinj  47869  fundcmpsurbijinj  47870  sprid  47934  stgr1  48437  setrec2  50170