Theorem abbii 2798

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

Syntax hints:   ↔ wb 206   = wceq 1541  {cab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723

This theorem is referenced by:  rabrab  3419  dfv2  3439  rabab  3467  csb2  3847  cbvcsbw  3855  cbvcsb  3856  cbvcsbv  3857  csbid  3858  csbcow  3860  csbco  3861  csbconstg  3864  csbie  3880  cbvreucsf  3889  unabw  4254  notabw  4260  unrab  4262  inrab  4263  inrab2  4264  difrab  4265  rabun2  4271  dfnul4  4282  dfnul2  4283  dfnul3  4284  abf  4353  dfif2  4474  dfsn2ALT  4595  rabsnifsb  4672  tprot  4699  pw0  4761  pwpw0  4762  dfopif  4819  pwsn  4849  dfuni2  4858  dfint2  4897  dfiunv2  4982  cbviun  4983  cbviin  4984  cbviung  4985  cbviing  4986  cbviunv  4987  cbviinv  4988  iunrab  4999  viin  5011  iunsn  5012  iinuni  5044  cbvopab  5161  cbvopabv  5162  cbvopab1  5163  cbvopab1g  5164  cbvopab2  5165  cbvopab1s  5166  cbvopab1v  5167  cbvopab2v  5168  unopab  5169  zfrep4  5229  zfpair  5357  iunopab  5497  dfid2  5511  dfid3  5512  rabxp  5662  csbxp  5715  dfdm3  5826  dfrn2  5827  dfrn3  5828  dfdm4  5834  dfdmf  5835  csbdm  5836  dmun  5849  dmopab  5854  dmopabss  5857  dmopab3  5858  dfrnf  5889  rnopab  5893  rnopabss  5894  rnopab3  5895  rnmpt  5896  dfima2  6010  dfima3  6011  imadmrn  6018  imai  6022  args  6040  mptpreima  6185  dfiota2  6438  cbviotaw  6444  cbviotavw  6445  cbviota  6446  sb8iota  6448  mptfnf  6616  dffv4  6819  dfimafn2  6885  opabiotadm  6903  fndmin  6978  dffo3f  7039  fnasrn  7078  elabrex  7176  elabrexg  7177  abrexco  7178  dfoprab2  7404  cbvoprab2  7434  cbvoprab12v  7436  cbvoprab3v  7438  dmoprab  7449  rnoprab  7451  rnoprab2  7452  fnrnov  7519  abnex  7690  uniuni  7695  zfrep6  7887  fvresex  7892  abrexex2g  7896  abexssex  7902  abexex  7903  oprabrexex2  7910  dfopab2  7984  poseq  8088  soseq  8089  suppvalbr  8094  cnvimadfsn  8102  dfrecs3  8292  rdglem1  8334  snec  8702  pmex  8755  fset0  8778  f1setex  8781  0map0sn0  8809  dfixp  8823  cbvixp  8838  cbvixpv  8839  pwfir  9201  marypha2lem4  9322  tcsni  9631  scottexs  9780  scott0s  9781  kardex  9787  cardf2  9836  dfac3  10012  infmap2  10108  cf0  10142  cfval2  10151  isf33lem  10257  dffin1-5  10279  axdc2lem  10339  addcompr  10912  mulcompr  10914  dfnn3  12139  hashf1lem2  14363  prprrab  14380  cshwsexa  14731  trclun  14921  shftdm  14978  hashbc0  16917  lubfval  18254  glbfval  18267  odulub  18311  oduglb  18313  symgbas0  19301  symgsubmefmnd  19310  pmtrprfvalrn  19400  efgval2  19636  dvdsrval  20279  dfrhm2  20392  toponsspwpw  22837  tgval2  22871  tgdif0  22907  xkobval  23501  ustfn  24117  ustn0  24136  2lgslem1b  27330  2sq  27368  madeval2  27794  addsasslem1  27946  addsasslem2  27947  negsid  27983  addsdilem1  28090  addsdilem2  28091  mulsasslem1  28102  mulsasslem2  28103  1p1e2s  28339  twocut  28346  pw2cut2  28382  0reno  28399  rusgrprc  29569  rgrprcx  29571  wwlksnfi  29884  clwwlkvbij  30093  dfconngr1  30168  isconngr  30169  isconngr1  30170  nmopnegi  31945  nmop0  31966  nmfn0  31967  sa-abvi  32423  dmrab  32476  abrexdomjm  32487  abrexexd  32489  cbviunf  32535  dfimafnf  32618  ofpreima  32647  intimafv  32692  maprnin  32714  fpwrelmapffslem  32715  hasheuni  34098  sigaex  34123  sigaval  34124  eulerpartlemt  34384  bnj1146  34803  bnj1400  34847  bnj882  34938  bnj893  34940  dfacycgr1  35188  derang0  35213  subfaclefac  35220  satfdm  35413  fmla0  35426  fmlasuc0  35428  fmla1  35431  dfon2lem7  35831  dfon2  35834  dfrdg2  35837  dfiota3  35965  fvline  36186  ellines  36194  sbceqbii  36233  rabeqbii  36236  iuneq12i  36237  iineq1i  36238  iineq12i  36239  ixpeq1i  36242  cbvcsbvw2  36273  cbviunvw2  36274  cbviinvw2  36275  cbvoprab1vw  36279  cbvoprab2vw  36280  cbvoprab123vw  36281  cbvoprab23vw  36282  cbvoprab13vw  36283  cbvixpvw2  36287  bj-df-ifc  36622  bj-dfif  36623  bj-rababw  36923  bj-inrab  36969  bj-taginv  37028  bj-nuliotaALT  37100  bj-dfid2ALT  37107  rnmptsn  37377  dissneqlem  37382  dissneq  37383  dffinxpf  37427  rabiun  37641  ismblfin  37709  volsupnfl  37713  areacirclem5  37760  abrexdom  37778  sdclem1  37791  sdc  37792  rncnvepres  38345  qsresid  38367  dmxrn  38414  dmcnvep  38415  rnxrn  38438  rncossdmcoss  38500  dfcoeleqvrels  38666  mpets  38888  psubspset  39791  pmapglb  39817  polval2N  39953  psubclsetN  39983  tendoset  40806  sticksstones16  42203  sticksstones21  42208  imaopab  42272  prjspeclsp  42653  sn-isghm  42714  eq0rabdioph  42817  rexrabdioph  42835  eldioph4b  42852  hbtlem6  43170  onsucrn  43312  dfno2  43469  alephiso2  43599  dfid7  43653  clcnvlem  43664  dfrtrcl5  43670  relopabVD  44941  iuneq1i  45130  dfaiota2  47125  dfaimafn2  47205  fundcmpsurinj  47448  fundcmpsurbijinj  47449  sprid  47513  stgr1  48000  setrec2  49735