Theorem abbii 2830

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755

This theorem is used by:  dfv2  3457  rabab  3484  csb2  3853  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbid  3864  csbcow  3866  csbco  3867  csbconstg  3870  csbie  3886  cbvreucsf  3895  unabw  4255  notabw  4261  unrab  4263  inrab  4264  inrab2  4265  difrab  4266  rabun2  4272  dfnul4  4283  dfnul2  4284  dfnul3  4285  abf  4367  dfif2  4487  dfsn2ALT  4606  rabsnifsb  4685  tprot  4712  pwsn  4832  pw0  4835  pwpw0  4836  dfopif  4842  dfuni2  4874  dfint2  4914  dfiunv2  4997  cbviun  4998  cbviin  4999  cbviung  5000  cbviing  5001  cbviunv  5002  cbviinv  5003  iunrab  5016  viin  5028  iunsn  5029  iinuni  5063  cbvopab  5183  cbvopabv  5184  cbvopab1  5185  cbvopab1g  5186  cbvopab2  5187  cbvopab1s  5188  cbvopab1v  5189  cbvopab2v  5190  unopab  5191  zfrep4  5252  zfpair  5390  iunopab  5541  dfid2  5555  dfid3  5556  rabxp  5706  csbxp  5760  relopabi  5809  dfdm3  5881  dfrn2  5882  dfrn3  5883  dfdm4  5889  dfdmf  5890  csbdm  5891  dmun  5904  dmopab  5909  dmopabss  5912  dmopab3  5913  dfrnf  5944  rnopab  5948  rnopabss  5949  rnopab3  5950  rnmpt  5951  dfima2  6076  dfima3  6077  imadmrnOLD  6086  imai  6090  args  6108  mptpreima  6258  dfiota2  6521  cbviotaw  6527  cbviotavw  6528  cbviota  6529  sb8iota  6531  mptfnf  6704  dffv4  6913  dfimafn2  6979  opabiotadm  6997  fndmin  7075  dffo3f  7138  fnasrn  7180  elabrex  7277  elabrexg  7278  abrexco  7279  dfoprab2  7509  cbvoprab2  7539  cbvoprab12v  7541  cbvoprab3v  7543  dmoprab  7554  rnoprab  7556  rnoprab2  7557  fnrnov  7626  abnex  7803  uniuni  7808  zfrep6OLD  8001  fvresex  8006  abrexex2g  8010  abexssex  8016  abexex  8017  oprabrexex2  8024  dfopab2  8098  poseq  8212  soseq  8213  suppvalbr  8218  suppvalbrOLD  8219  cnvimadfsn  8227  dfrecs3  8418  rdglem1  8461  snec  8837  pmex  8890  fset0  8914  f1setex  8917  0map0sn0  8951  dfixp  8965  cbvixp  8980  cbvixpv  8981  pwfir  9346  marypha2lem4  9467  tcsni  9779  scottexsOLD  9980  scott0bsOLD  9982  kardexOLD  9995  setrec2  10014  cardf2  10061  dfac3  10239  infmap2  10334  cf0  10367  cfval2  10377  isf33lem  10483  dffin1-5  10505  axdc2lem  10565  addcompr  11145  mulcompr  11147  dfnn3  12389  hashf1lem2  14642  prprrab  14659  cshwsexa  15017  trclun  15210  shftdm  15267  hashbc0  17227  lubfval  18572  glbfval  18585  odulub  18629  oduglb  18631  symgbas0  19654  symgsubmefmnd  19663  pmtrprfvalrn  19753  efgval2  19989  dvdsrval  20642  dfrhm2  20755  toponsspwpw  23295  tgval2  23329  tgdif0  23365  xkobval  23960  ustfn  24576  ustn0  24595  2lgslem1b  27776  2sq  27814  madeval2  28276  addsasslem1  28446  addsasslem2  28447  negsid  28484  addsdilem1  28594  addsdilem2  28595  mulsasslem1  28606  mulsasslem2  28607  twocut  28866  pw2cut2  28905  rusgrprc  30228  rgrprcx  30230  wwlksnfi  30552  clwwlkvbij  30761  dfacycgr1  30807  dfconngr1  30846  isconngr  30847  isconngr1  30848  nmopnegi  32624  nmop0  32645  nmfn0  32646  sa-abvi  33144  dmrab  33192  abrexdomjm  33202  abrexexd  33204  cbviunf  33248  dfimafnf  33328  ofpreima  33357  intimafv  33401  maprnin  33419  fpwrelmapffslem  33420  hasheuni  34828  sigaex  34853  sigaval  34854  eulerpartlemt  35114  bnj1146  35532  bnj1400  35576  bnj882  35667  bnj893  35669  derang0  36142  subfaclefac  36149  satfdm  36342  fmla0  36355  fmlasuc0  36357  fmla1  36360  dfon2lem7  36766  dfon2  36769  dfrdg2  36772  dfiota3  36900  fvline  37124  ellines  37132  sbceqbii  37195  rabeqbii  37198  iuneq12i  37199  iineq1i  37200  iineq12i  37201  ixpeq1i  37204  cbvcsbvw2  37235  cbviunvw2  37236  cbviinvw2  37237  cbvoprab1vw  37241  cbvoprab2vw  37242  cbvoprab123vw  37243  cbvoprab23vw  37244  cbvoprab13vw  37245  cbvixpvw2  37249  bj-dfnul2  37655  bj-df-ifc  37665  bj-dfif  37666  bj-rababw  38008  bj-inrab  38055  bj-taginv  38114  bj-nuliotaALT  38243  bj-dfid2ALT  38250  rnmptsn  38526  dissneqlem  38531  dissneq  38532  dffinxpf  38576  rabiun  38789  ismblfin  38847  volsupnfl  38851  areacirclem5  38898  dfproplem  38909  abrexdom  38932  sdclem1  38943  sdc  38944  rncnvepres  39507  qsresid  39529  dmxrn  39585  dmcnvep  39586  rnxrn  39619  dfsuccl3  39671  dfsuccl4  39672  rncossdmcoss  39743  dfcoeleqvrels  39903  mpets  40154  psubspset  41067  pmapglb  41093  polval2N  41229  psubclsetN  41259  tendoset  42082  sticksstones16  43478  sticksstones21  43483  imaopab  43552  prjspeclsp  43906  sn-isghm  43950  eq0rabdioph  44053  rexrabdioph  44067  eldioph4b  44084  hbtlem6  44396  onsucrn  44534  dfno2  44690  alephiso2  44820  dfid7  44873  clcnvlem  44884  dfrtrcl5  44890  relopabVD  46143  iuneq1i  46374  dfaiota2  48429  dfaimafn2  48509  fundcmpsurinj  48764  fundcmpsurbijinj  48765  sprid  48829  stgr1  49332