Theorem abbii 2801

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

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

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 2123  ax-ext 2706

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

This theorem is referenced by:  rabrab  3421  dfv2  3441  rabab  3469  csb2  3849  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbid  3860  csbcow  3862  csbco  3863  csbconstg  3866  csbie  3882  cbvreucsf  3891  unabw  4257  notabw  4263  unrab  4265  inrab  4266  inrab2  4267  difrab  4268  rabun2  4274  dfnul4  4285  dfnul2  4286  dfnul3  4287  abf  4356  dfif2  4479  dfsn2ALT  4600  rabsnifsb  4677  tprot  4704  pw0  4766  pwpw0  4767  dfopif  4824  pwsn  4854  dfuni2  4863  dfint2  4902  dfiunv2  4987  cbviun  4988  cbviin  4989  cbviung  4990  cbviing  4991  cbviunv  4992  cbviinv  4993  iunrab  5006  viin  5018  iunsn  5019  iinuni  5051  cbvopab  5168  cbvopabv  5169  cbvopab1  5170  cbvopab1g  5171  cbvopab2  5172  cbvopab1s  5173  cbvopab1v  5174  cbvopab2v  5175  unopab  5176  zfrep4  5236  zfpair  5364  iunopab  5505  dfid2  5519  dfid3  5520  rabxp  5670  csbxp  5723  dfdm3  5834  dfrn2  5835  dfrn3  5836  dfdm4  5842  dfdmf  5843  csbdm  5844  dmun  5857  dmopab  5862  dmopabss  5865  dmopab3  5866  dfrnf  5897  rnopab  5901  rnopabss  5902  rnopab3  5903  rnmpt  5904  dfima2  6019  dfima3  6020  imadmrn  6027  imai  6031  args  6049  mptpreima  6194  dfiota2  6447  cbviotaw  6453  cbviotavw  6454  cbviota  6455  sb8iota  6457  mptfnf  6625  dffv4  6829  dfimafn2  6895  opabiotadm  6913  fndmin  6988  dffo3f  7049  fnasrn  7088  elabrex  7186  elabrexg  7187  abrexco  7188  dfoprab2  7414  cbvoprab2  7444  cbvoprab12v  7446  cbvoprab3v  7448  dmoprab  7459  rnoprab  7461  rnoprab2  7462  fnrnov  7529  abnex  7700  uniuni  7705  zfrep6  7897  fvresex  7902  abrexex2g  7906  abexssex  7912  abexex  7913  oprabrexex2  7920  dfopab2  7994  poseq  8098  soseq  8099  suppvalbr  8104  cnvimadfsn  8112  dfrecs3  8302  rdglem1  8344  snec  8713  pmex  8766  fset0  8789  f1setex  8792  0map0sn0  8821  dfixp  8835  cbvixp  8850  cbvixpv  8851  pwfir  9215  marypha2lem4  9339  tcsni  9648  scottexs  9797  scott0s  9798  kardex  9804  cardf2  9853  dfac3  10029  infmap2  10125  cf0  10159  cfval2  10168  isf33lem  10274  dffin1-5  10296  axdc2lem  10356  addcompr  10930  mulcompr  10932  dfnn3  12157  hashf1lem2  14377  prprrab  14394  cshwsexa  14745  trclun  14935  shftdm  14992  hashbc0  16931  lubfval  18269  glbfval  18282  odulub  18326  oduglb  18328  symgbas0  19316  symgsubmefmnd  19325  pmtrprfvalrn  19415  efgval2  19651  dvdsrval  20295  dfrhm2  20408  toponsspwpw  22864  tgval2  22898  tgdif0  22934  xkobval  23528  ustfn  24144  ustn0  24163  2lgslem1b  27357  2sq  27395  madeval2  27821  addsasslem1  27973  addsasslem2  27974  negsid  28010  addsdilem1  28120  addsdilem2  28121  mulsasslem1  28132  mulsasslem2  28133  1p1e2s  28374  twocut  28381  pw2cut2  28419  rusgrprc  29613  rgrprcx  29615  wwlksnfi  29928  clwwlkvbij  30137  dfconngr1  30212  isconngr  30213  isconngr1  30214  nmopnegi  31989  nmop0  32010  nmfn0  32011  sa-abvi  32467  dmrab  32520  abrexdomjm  32531  abrexexd  32533  cbviunf  32579  dfimafnf  32663  ofpreima  32692  intimafv  32739  maprnin  32759  fpwrelmapffslem  32760  hasheuni  34191  sigaex  34216  sigaval  34217  eulerpartlemt  34477  bnj1146  34896  bnj1400  34940  bnj882  35031  bnj893  35033  dfacycgr1  35287  derang0  35312  subfaclefac  35319  satfdm  35512  fmla0  35525  fmlasuc0  35527  fmla1  35530  dfon2lem7  35930  dfon2  35933  dfrdg2  35936  dfiota3  36064  fvline  36287  ellines  36295  sbceqbii  36334  rabeqbii  36337  iuneq12i  36338  iineq1i  36339  iineq12i  36340  ixpeq1i  36343  cbvcsbvw2  36374  cbviunvw2  36375  cbviinvw2  36376  cbvoprab1vw  36380  cbvoprab2vw  36381  cbvoprab123vw  36382  cbvoprab23vw  36383  cbvoprab13vw  36384  cbvixpvw2  36388  bj-df-ifc  36723  bj-dfif  36724  bj-rababw  37025  bj-inrab  37071  bj-taginv  37130  bj-nuliotaALT  37202  bj-dfid2ALT  37209  rnmptsn  37479  dissneqlem  37484  dissneq  37485  dffinxpf  37529  rabiun  37733  ismblfin  37801  volsupnfl  37805  areacirclem5  37852  abrexdom  37870  sdclem1  37883  sdc  37884  rncnvepres  38441  qsresid  38463  dmxrn  38511  dmcnvep  38512  rnxrn  38545  dfsuccl3  38586  dfsuccl4  38587  rncossdmcoss  38657  dfcoeleqvrels  38817  mpets  39040  psubspset  39943  pmapglb  39969  polval2N  40105  psubclsetN  40135  tendoset  40958  sticksstones16  42355  sticksstones21  42360  imaopab  42429  prjspeclsp  42797  sn-isghm  42858  eq0rabdioph  42960  rexrabdioph  42978  eldioph4b  42995  hbtlem6  43313  onsucrn  43455  dfno2  43611  alephiso2  43741  dfid7  43795  clcnvlem  43806  dfrtrcl5  43812  relopabVD  45083  iuneq1i  45271  dfaiota2  47274  dfaimafn2  47354  fundcmpsurinj  47597  fundcmpsurbijinj  47598  sprid  47662  stgr1  48149  setrec2  49882