Theorem abbii 2804

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

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

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 2709

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

This theorem is referenced by:  dfv2  3433  rabab  3461  csb2  3840  cbvcsbw  3848  cbvcsb  3849  cbvcsbv  3850  csbid  3851  csbcow  3853  csbco  3854  csbconstg  3857  csbie  3873  cbvreucsf  3882  unabw  4248  notabw  4254  unrab  4256  inrab  4257  inrab2  4258  difrab  4259  rabun2  4265  dfnul4  4276  dfnul2  4277  dfnul3  4278  abf  4347  dfif2  4469  dfsn2ALT  4590  rabsnifsb  4667  tprot  4694  pw0  4756  pwpw0  4757  dfopif  4814  pwsn  4844  dfuni2  4853  dfint2  4892  dfiunv2  4977  cbviun  4978  cbviin  4979  cbviung  4980  cbviing  4981  cbviunv  4982  cbviinv  4983  iunrab  4996  viin  5008  iunsn  5009  iinuni  5041  cbvopab  5158  cbvopabv  5159  cbvopab1  5160  cbvopab1g  5161  cbvopab2  5162  cbvopab1s  5163  cbvopab1v  5164  cbvopab2v  5165  unopab  5166  zfrep4  5229  zfpair  5359  iunopab  5508  dfid2  5522  dfid3  5523  rabxp  5673  csbxp  5726  dfdm3  5837  dfrn2  5838  dfrn3  5839  dfdm4  5845  dfdmf  5846  csbdm  5847  dmun  5860  dmopab  5865  dmopabss  5868  dmopab3  5869  dfrnf  5900  rnopab  5904  rnopabss  5905  rnopab3  5906  rnmpt  5907  dfima2  6022  dfima3  6023  imadmrn  6030  imai  6034  args  6052  mptpreima  6197  dfiota2  6450  cbviotaw  6456  cbviotavw  6457  cbviota  6458  sb8iota  6460  mptfnf  6628  dffv4  6832  dfimafn2  6898  opabiotadm  6916  fndmin  6992  dffo3f  7053  fnasrn  7093  elabrex  7191  elabrexg  7192  abrexco  7193  dfoprab2  7419  cbvoprab2  7449  cbvoprab12v  7451  cbvoprab3v  7453  dmoprab  7464  rnoprab  7466  rnoprab2  7467  fnrnov  7534  abnex  7705  uniuni  7710  zfrep6OLD  7902  fvresex  7907  abrexex2g  7911  abexssex  7917  abexex  7918  oprabrexex2  7925  dfopab2  7999  poseq  8102  soseq  8103  suppvalbr  8108  cnvimadfsn  8116  dfrecs3  8306  rdglem1  8348  snec  8719  pmex  8772  fset0  8795  f1setex  8798  0map0sn0  8827  dfixp  8841  cbvixp  8856  cbvixpv  8857  pwfir  9221  marypha2lem4  9345  tcsni  9656  scottexs  9805  scott0s  9806  kardex  9812  cardf2  9861  dfac3  10037  infmap2  10133  cf0  10167  cfval2  10176  isf33lem  10282  dffin1-5  10304  axdc2lem  10364  addcompr  10938  mulcompr  10940  dfnn3  12182  hashf1lem2  14412  prprrab  14429  cshwsexa  14780  trclun  14970  shftdm  15027  hashbc0  16970  lubfval  18308  glbfval  18321  odulub  18365  oduglb  18367  symgbas0  19358  symgsubmefmnd  19367  pmtrprfvalrn  19457  efgval2  19693  dvdsrval  20335  dfrhm2  20448  toponsspwpw  22900  tgval2  22934  tgdif0  22970  xkobval  23564  ustfn  24180  ustn0  24199  2lgslem1b  27372  2sq  27410  madeval2  27842  addsasslem1  28012  addsasslem2  28013  negsid  28050  addsdilem1  28160  addsdilem2  28161  mulsasslem1  28172  mulsasslem2  28173  twocut  28432  pw2cut2  28471  rusgrprc  29677  rgrprcx  29679  wwlksnfi  29992  clwwlkvbij  30201  dfconngr1  30276  isconngr  30277  isconngr1  30278  nmopnegi  32054  nmop0  32075  nmfn0  32076  sa-abvi  32532  dmrab  32584  abrexdomjm  32595  abrexexd  32597  cbviunf  32643  dfimafnf  32727  ofpreima  32756  intimafv  32802  maprnin  32822  fpwrelmapffslem  32823  hasheuni  34248  sigaex  34273  sigaval  34274  eulerpartlemt  34534  bnj1146  34952  bnj1400  34996  bnj882  35087  bnj893  35089  dfacycgr1  35345  derang0  35370  subfaclefac  35377  satfdm  35570  fmla0  35583  fmlasuc0  35585  fmla1  35588  dfon2lem7  35988  dfon2  35991  dfrdg2  35994  dfiota3  36122  fvline  36345  ellines  36353  sbceqbii  36392  rabeqbii  36395  iuneq12i  36396  iineq1i  36397  iineq12i  36398  ixpeq1i  36401  cbvcsbvw2  36432  cbviunvw2  36433  cbviinvw2  36434  cbvoprab1vw  36438  cbvoprab2vw  36439  cbvoprab123vw  36440  cbvoprab23vw  36441  cbvoprab13vw  36442  cbvixpvw2  36446  bj-dfnul2  36854  bj-df-ifc  36864  bj-dfif  36865  bj-rababw  37207  bj-inrab  37253  bj-taginv  37312  bj-nuliotaALT  37384  bj-dfid2ALT  37391  rnmptsn  37668  dissneqlem  37673  dissneq  37674  dffinxpf  37718  rabiun  37931  ismblfin  37999  volsupnfl  38003  areacirclem5  38050  abrexdom  38068  sdclem1  38081  sdc  38082  rncnvepres  38647  qsresid  38669  dmxrn  38725  dmcnvep  38726  rnxrn  38759  dfsuccl3  38811  dfsuccl4  38812  rncossdmcoss  38883  dfcoeleqvrels  39043  mpets  39294  psubspset  40207  pmapglb  40233  polval2N  40369  psubclsetN  40399  tendoset  41222  sticksstones16  42618  sticksstones21  42623  imaopab  42689  prjspeclsp  43062  sn-isghm  43123  eq0rabdioph  43225  rexrabdioph  43243  eldioph4b  43260  hbtlem6  43578  onsucrn  43720  dfno2  43876  alephiso2  44006  dfid7  44060  clcnvlem  44071  dfrtrcl5  44077  relopabVD  45348  iuneq1i  45536  dfaiota2  47549  dfaimafn2  47629  fundcmpsurinj  47884  fundcmpsurbijinj  47885  sprid  47949  stgr1  48452  setrec2  50185