Theorem abbii 2828

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753

This theorem is used by:  dfv2  3454  rabab  3481  csb2  3849  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbid  3860  csbcow  3862  csbco  3863  csbconstg  3866  csbie  3882  cbvreucsf  3891  unabw  4253  notabw  4259  unrab  4261  inrab  4262  inrab2  4263  difrab  4264  rabun2  4270  dfnul4  4281  dfnul2  4282  dfnul3  4283  abf  4364  dfif2  4484  dfsn2ALT  4606  rabsnifsb  4683  tprot  4710  pw0  4773  pwpw0  4774  dfopif  4830  pwsn  4860  dfuni2  4869  dfint2  4909  dfiunv2  4992  cbviun  4993  cbviin  4994  cbviung  4995  cbviing  4996  cbviunv  4997  cbviinv  4998  iunrab  5011  viin  5023  iunsn  5024  iinuni  5058  cbvopab  5177  cbvopabv  5178  cbvopab1  5179  cbvopab1g  5180  cbvopab2  5181  cbvopab1s  5182  cbvopab1v  5183  cbvopab2v  5184  unopab  5185  zfrep4  5246  zfpair  5383  iunopab  5534  dfid2  5548  dfid3  5549  rabxp  5699  csbxp  5752  dfdm3  5869  dfrn2  5870  dfrn3  5871  dfdm4  5877  dfdmf  5878  csbdm  5879  dmun  5892  dmopab  5897  dmopabss  5900  dmopab3  5901  dfrnf  5932  rnopab  5936  rnopabss  5937  rnopab3  5938  rnmpt  5939  dfima2  6058  dfima3  6059  imadmrnOLD  6068  imai  6072  args  6090  mptpreima  6238  dfiota2  6494  cbviotaw  6500  cbviotavw  6501  cbviota  6502  sb8iota  6504  mptfnf  6672  dffv4  6880  dfimafn2  6946  opabiotadm  6964  fndmin  7042  dffo3f  7104  fnasrn  7146  elabrex  7244  elabrexg  7245  abrexco  7246  dfoprab2  7476  cbvoprab2  7506  cbvoprab12v  7508  cbvoprab3v  7510  dmoprab  7521  rnoprab  7523  rnoprab2  7524  fnrnov  7592  abnex  7769  uniuni  7774  zfrep6OLD  7965  fvresex  7970  abrexex2g  7974  abexssex  7980  abexex  7981  oprabrexex2  7988  dfopab2  8061  poseq  8168  soseq  8169  suppvalbr  8174  cnvimadfsn  8182  dfrecs3  8373  rdglem1  8416  snec  8792  pmex  8845  fset0  8869  f1setex  8872  0map0sn0  8906  dfixp  8920  cbvixp  8935  cbvixpv  8936  pwfir  9301  marypha2lem4  9423  tcsni  9735  scottexsOLD  9936  scott0bsOLD  9938  kardexOLD  9951  setrec2  9970  cardf2  10017  dfac3  10193  infmap2  10288  cf0  10321  cfval2  10331  isf33lem  10437  dffin1-5  10459  axdc2lem  10519  addcompr  11099  mulcompr  11101  dfnn3  12342  hashf1lem2  14594  prprrab  14611  cshwsexa  14968  trclun  15160  shftdm  15217  hashbc0  17176  lubfval  18515  glbfval  18528  odulub  18572  oduglb  18574  symgbas0  19596  symgsubmefmnd  19605  pmtrprfvalrn  19695  efgval2  19931  dvdsrval  20584  dfrhm2  20697  toponsspwpw  23233  tgval2  23267  tgdif0  23303  xkobval  23898  ustfn  24514  ustn0  24533  2lgslem1b  27712  2sq  27750  madeval2  28212  addsasslem1  28382  addsasslem2  28383  negsid  28420  addsdilem1  28530  addsdilem2  28531  mulsasslem1  28542  mulsasslem2  28543  twocut  28802  pw2cut2  28841  rusgrprc  30164  rgrprcx  30166  wwlksnfi  30488  clwwlkvbij  30697  dfacycgr1  30743  dfconngr1  30782  isconngr  30783  isconngr1  30784  nmopnegi  32560  nmop0  32581  nmfn0  32582  sa-abvi  33038  dmrab  33086  abrexdomjm  33096  abrexexd  33098  cbviunf  33143  dfimafnf  33223  ofpreima  33252  intimafv  33297  maprnin  33316  fpwrelmapffslem  33317  hasheuni  34710  sigaex  34735  sigaval  34736  eulerpartlemt  34996  bnj1146  35414  bnj1400  35458  bnj882  35549  bnj893  35551  derang0  35913  subfaclefac  35920  satfdm  36113  fmla0  36126  fmlasuc0  36128  fmla1  36131  dfon2lem7  36531  dfon2  36534  dfrdg2  36537  dfiota3  36665  fvline  36889  ellines  36897  sbceqbii  36960  rabeqbii  36963  iuneq12i  36964  iineq1i  36965  iineq12i  36966  ixpeq1i  36969  cbvcsbvw2  37000  cbviunvw2  37001  cbviinvw2  37002  cbvoprab1vw  37006  cbvoprab2vw  37007  cbvoprab123vw  37008  cbvoprab23vw  37009  cbvoprab13vw  37010  cbvixpvw2  37014  bj-dfnul2  37420  bj-df-ifc  37430  bj-dfif  37431  bj-rababw  37773  bj-inrab  37820  bj-taginv  37879  bj-nuliotaALT  37953  bj-dfid2ALT  37960  rnmptsn  38238  dissneqlem  38243  dissneq  38244  dffinxpf  38288  rabiun  38501  ismblfin  38559  volsupnfl  38563  areacirclem5  38610  dfproplem  38621  abrexdom  38644  sdclem1  38657  sdc  38658  rncnvepres  39221  qsresid  39243  dmxrn  39299  dmcnvep  39300  rnxrn  39333  dfsuccl3  39385  dfsuccl4  39386  rncossdmcoss  39457  dfcoeleqvrels  39617  mpets  39868  psubspset  40781  pmapglb  40807  polval2N  40943  psubclsetN  40973  tendoset  41796  sticksstones16  43192  sticksstones21  43197  imaopab  43265  prjspeclsp  43620  sn-isghm  43664  eq0rabdioph  43766  rexrabdioph  43780  eldioph4b  43797  hbtlem6  44115  onsucrn  44257  dfno2  44413  alephiso2  44543  dfid7  44597  clcnvlem  44608  dfrtrcl5  44614  relopabVD  45868  iuneq1i  46070  dfaiota2  48125  dfaimafn2  48205  fundcmpsurinj  48460  fundcmpsurbijinj  48461  sprid  48525  stgr1  49028