Theorem abbii 2827

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752

This theorem is used by:  dfv2  3453  rabab  3480  csb2  3849  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbid  3860  csbcow  3862  csbco  3863  csbconstg  3866  csbie  3882  cbvreucsf  3891  unabw  4251  notabw  4257  unrab  4259  inrab  4260  inrab2  4261  difrab  4262  rabun2  4268  dfnul4  4279  dfnul2  4280  dfnul3  4281  abf  4363  dfif2  4483  dfsn2ALT  4602  rabsnifsb  4679  tprot  4706  pwsn  4826  pw0  4829  pwpw0  4830  dfopif  4836  dfuni2  4868  dfint2  4908  dfiunv2  4991  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  cbviunv  4996  cbviinv  4997  iunrab  5010  viin  5022  iunsn  5023  iinuni  5057  cbvopab  5176  cbvopabv  5177  cbvopab1  5178  cbvopab1g  5179  cbvopab2  5180  cbvopab1s  5181  cbvopab1v  5182  cbvopab2v  5183  unopab  5184  zfrep4  5245  zfpair  5383  iunopab  5534  dfid2  5548  dfid3  5549  rabxp  5699  csbxp  5753  dfdm3  5870  dfrn2  5871  dfrn3  5872  dfdm4  5878  dfdmf  5879  csbdm  5880  dmun  5893  dmopab  5898  dmopabss  5901  dmopab3  5902  dfrnf  5933  rnopab  5937  rnopabss  5938  rnopab3  5939  rnmpt  5940  dfima2  6060  dfima3  6061  imadmrnOLD  6070  imai  6074  args  6092  mptpreima  6242  dfiota2  6498  cbviotaw  6504  cbviotavw  6505  cbviota  6506  sb8iota  6508  mptfnf  6679  dffv4  6887  dfimafn2  6953  opabiotadm  6971  fndmin  7049  dffo3f  7111  fnasrn  7153  elabrex  7250  elabrexg  7251  abrexco  7252  dfoprab2  7482  cbvoprab2  7512  cbvoprab12v  7514  cbvoprab3v  7516  dmoprab  7527  rnoprab  7529  rnoprab2  7530  fnrnov  7598  abnex  7775  uniuni  7780  zfrep6OLD  7971  fvresex  7976  abrexex2g  7980  abexssex  7986  abexex  7987  oprabrexex2  7994  dfopab2  8067  poseq  8181  soseq  8182  suppvalbr  8187  suppvalbrOLD  8188  cnvimadfsn  8196  dfrecs3  8387  rdglem1  8430  snec  8806  pmex  8859  fset0  8883  f1setex  8886  0map0sn0  8920  dfixp  8934  cbvixp  8949  cbvixpv  8950  pwfir  9315  marypha2lem4  9437  tcsni  9749  scottexsOLD  9950  scott0bsOLD  9952  kardexOLD  9965  setrec2  9984  cardf2  10031  dfac3  10207  infmap2  10302  cf0  10335  cfval2  10345  isf33lem  10451  dffin1-5  10473  axdc2lem  10533  addcompr  11113  mulcompr  11115  dfnn3  12356  hashf1lem2  14608  prprrab  14625  cshwsexa  14983  trclun  15176  shftdm  15233  hashbc0  17192  lubfval  18531  glbfval  18544  odulub  18588  oduglb  18590  symgbas0  19612  symgsubmefmnd  19621  pmtrprfvalrn  19711  efgval2  19947  dvdsrval  20600  dfrhm2  20713  toponsspwpw  23249  tgval2  23283  tgdif0  23319  xkobval  23914  ustfn  24530  ustn0  24549  2lgslem1b  27728  2sq  27766  madeval2  28228  addsasslem1  28398  addsasslem2  28399  negsid  28436  addsdilem1  28546  addsdilem2  28547  mulsasslem1  28558  mulsasslem2  28559  twocut  28818  pw2cut2  28857  rusgrprc  30180  rgrprcx  30182  wwlksnfi  30504  clwwlkvbij  30713  dfacycgr1  30759  dfconngr1  30798  isconngr  30799  isconngr1  30800  nmopnegi  32576  nmop0  32597  nmfn0  32598  sa-abvi  33096  dmrab  33144  abrexdomjm  33154  abrexexd  33156  cbviunf  33201  dfimafnf  33281  ofpreima  33310  intimafv  33355  maprnin  33373  fpwrelmapffslem  33374  hasheuni  34767  sigaex  34792  sigaval  34793  eulerpartlemt  35053  bnj1146  35471  bnj1400  35515  bnj882  35606  bnj893  35608  derang0  36024  subfaclefac  36031  satfdm  36224  fmla0  36237  fmlasuc0  36239  fmla1  36242  dfon2lem7  36647  dfon2  36650  dfrdg2  36653  dfiota3  36781  fvline  37005  ellines  37013  sbceqbii  37076  rabeqbii  37079  iuneq12i  37080  iineq1i  37081  iineq12i  37082  ixpeq1i  37085  cbvcsbvw2  37116  cbviunvw2  37117  cbviinvw2  37118  cbvoprab1vw  37122  cbvoprab2vw  37123  cbvoprab123vw  37124  cbvoprab23vw  37125  cbvoprab13vw  37126  cbvixpvw2  37130  bj-dfnul2  37536  bj-df-ifc  37546  bj-dfif  37547  bj-rababw  37889  bj-inrab  37936  bj-taginv  37995  bj-nuliotaALT  38081  bj-dfid2ALT  38088  rnmptsn  38367  dissneqlem  38372  dissneq  38373  dffinxpf  38417  rabiun  38630  ismblfin  38688  volsupnfl  38692  areacirclem5  38739  dfproplem  38750  abrexdom  38773  sdclem1  38786  sdc  38787  rncnvepres  39350  qsresid  39372  dmxrn  39428  dmcnvep  39429  rnxrn  39462  dfsuccl3  39514  dfsuccl4  39515  rncossdmcoss  39586  dfcoeleqvrels  39746  mpets  39997  psubspset  40910  pmapglb  40936  polval2N  41072  psubclsetN  41102  tendoset  41925  sticksstones16  43321  sticksstones21  43326  imaopab  43394  prjspeclsp  43749  sn-isghm  43793  eq0rabdioph  43896  rexrabdioph  43910  eldioph4b  43927  hbtlem6  44240  onsucrn  44382  dfno2  44538  alephiso2  44668  dfid7  44721  clcnvlem  44732  dfrtrcl5  44738  relopabVD  45991  iuneq1i  46209  dfaiota2  48264  dfaimafn2  48344  fundcmpsurinj  48599  fundcmpsurbijinj  48600  sprid  48664  stgr1  49167