Theorem abbii 2796

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

Syntax hints:   ↔ wb 206   = wceq 1540  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721

This theorem is referenced by:  rabbiiaOLD  3410  rabrab  3430  dfv2  3450  rabab  3478  csb2  3864  cbvcsbw  3872  cbvcsb  3873  cbvcsbv  3874  csbid  3875  csbcow  3877  csbco  3878  csbconstg  3881  csbie  3897  cbvreucsf  3906  unabw  4270  notabw  4276  unrab  4278  inrab  4279  inrab2  4280  difrab  4281  rabun2  4287  dfnul4  4298  dfnul2  4299  dfnul3  4300  abf  4369  dfif2  4490  dfsn2ALT  4611  rabsnifsb  4686  tprot  4713  pw0  4776  pwpw0  4777  dfopif  4834  pwsn  4864  dfuni2  4873  dfint2  4912  dfiunv2  4999  cbviun  5000  cbviin  5001  cbviung  5002  cbviing  5003  cbviunv  5004  cbviinv  5005  iunrab  5016  iunidOLD  5025  viin  5029  iunsn  5030  iinuni  5062  cbvopab  5179  cbvopabv  5180  cbvopab1  5181  cbvopab1g  5182  cbvopab2  5183  cbvopab1s  5184  cbvopab1v  5185  cbvopab2v  5186  unopab  5187  zfrep4  5248  zfpair  5376  iunopab  5519  iunopabOLD  5520  dfid2  5535  dfid3  5536  rabxp  5686  csbxp  5738  dfdm3  5851  dfrn2  5852  dfrn3  5853  dfdm4  5859  dfdmf  5860  csbdm  5861  dmun  5874  dmopab  5879  dmopabss  5882  dmopab3  5883  dfrnf  5914  rnopab  5918  rnopabss  5919  rnopab3  5920  rnmpt  5921  dfima2  6033  dfima3  6034  imadmrn  6041  imai  6045  args  6063  mptpreima  6211  dfiota2  6465  cbviotaw  6471  cbviotavw  6472  cbviota  6473  sb8iota  6475  mptfnf  6653  dffv4  6855  dfimafn2  6924  opabiotadm  6942  fndmin  7017  dffo3f  7078  fnasrn  7117  elabrex  7216  elabrexg  7217  abrexco  7218  dfoprab2  7447  cbvoprab2  7477  cbvoprab12v  7479  cbvoprab3v  7481  dmoprab  7492  rnoprab  7494  rnoprab2  7495  fnrnov  7562  abnex  7733  uniuni  7738  zfrep6  7933  fvresex  7938  abrexex2g  7943  abexssex  7949  abexex  7950  oprabrexex2  7957  dfopab2  8031  poseq  8137  soseq  8138  suppvalbr  8143  cnvimadfsn  8151  dfrecs3  8341  rdglem1  8383  snec  8751  pmex  8804  fset0  8827  f1setex  8830  0map0sn0  8858  dfixp  8872  cbvixp  8887  cbvixpv  8888  pwfir  9266  marypha2lem4  9389  tcsni  9696  scottexs  9840  scott0s  9841  kardex  9847  cardf2  9896  dfac3  10074  infmap2  10170  cf0  10204  cfval2  10213  isf33lem  10319  dffin1-5  10341  axdc2lem  10401  addcompr  10974  mulcompr  10976  dfnn3  12200  hashf1lem2  14421  prprrab  14438  cshwsexa  14789  cshwsexaOLD  14790  trclun  14980  shftdm  15037  hashbc0  16976  lubfval  18309  glbfval  18322  odulub  18366  oduglb  18368  symgbas0  19319  symgsubmefmnd  19328  pmtrprfvalrn  19418  efgval2  19654  dvdsrval  20270  dfrhm2  20383  toponsspwpw  22809  tgval2  22843  tgdif0  22879  xkobval  23473  ustfn  24089  ustn0  24108  2lgslem1b  27303  2sq  27341  madeval2  27761  addsasslem1  27910  addsasslem2  27911  negsid  27947  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  1p1e2s  28302  twocut  28309  0reno  28348  rusgrprc  29518  rgrprcx  29520  wwlksnfi  29836  clwwlkvbij  30042  dfconngr1  30117  isconngr  30118  isconngr1  30119  nmopnegi  31894  nmop0  31915  nmfn0  31916  sa-abvi  32372  dmrab  32426  abrexdomjm  32436  abrexexd  32438  cbviunf  32484  dfimafnf  32560  ofpreima  32589  intimafv  32634  maprnin  32654  fpwrelmapffslem  32655  hasheuni  34075  sigaex  34100  sigaval  34101  eulerpartlemt  34362  bnj1146  34781  bnj1400  34825  bnj882  34916  bnj893  34918  dfacycgr1  35131  derang0  35156  subfaclefac  35163  satfdm  35356  fmla0  35369  fmlasuc0  35371  fmla1  35374  dfon2lem7  35777  dfon2  35780  dfrdg2  35783  dfiota3  35911  fvline  36132  ellines  36140  sbceqbii  36179  rabeqbii  36182  iuneq12i  36183  iineq1i  36184  iineq12i  36185  ixpeq1i  36188  cbvcsbvw2  36219  cbviunvw2  36220  cbviinvw2  36221  cbvoprab1vw  36225  cbvoprab2vw  36226  cbvoprab123vw  36227  cbvoprab23vw  36228  cbvoprab13vw  36229  cbvixpvw2  36233  bj-df-ifc  36568  bj-dfif  36569  bj-rababw  36869  bj-inrab  36915  bj-taginv  36974  bj-nuliotaALT  37046  bj-dfid2ALT  37053  rnmptsn  37323  dissneqlem  37328  dissneq  37329  dffinxpf  37373  rabiun  37587  ismblfin  37655  volsupnfl  37659  areacirclem5  37706  abrexdom  37724  sdclem1  37737  sdc  37738  rncnvepres  38291  qsresid  38313  dmxrn  38360  dmcnvep  38361  rnxrn  38384  rncossdmcoss  38446  dfcoeleqvrels  38612  mpets  38834  psubspset  39738  pmapglb  39764  polval2N  39900  psubclsetN  39930  tendoset  40753  sticksstones16  42150  sticksstones21  42155  imaopab  42219  prjspeclsp  42600  sn-isghm  42661  eq0rabdioph  42764  rexrabdioph  42782  eldioph4b  42799  hbtlem6  43118  onsucrn  43260  dfno2  43417  alephiso2  43547  dfid7  43601  clcnvlem  43612  dfrtrcl5  43618  relopabVD  44890  iuneq1i  45079  dfaiota2  47087  dfaimafn2  47167  fundcmpsurinj  47410  fundcmpsurbijinj  47411  sprid  47475  stgr1  47960  setrec2  49684