Theorem abbii 2804

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

Syntax hints:   ↔ wb 206   = wceq 1542  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729

This theorem is referenced by:  rabrab  3425  dfv2  3445  rabab  3473  csb2  3853  cbvcsbw  3861  cbvcsb  3862  cbvcsbv  3863  csbid  3864  csbcow  3866  csbco  3867  csbconstg  3870  csbie  3886  cbvreucsf  3895  unabw  4261  notabw  4267  unrab  4269  inrab  4270  inrab2  4271  difrab  4272  rabun2  4278  dfnul4  4289  dfnul2  4290  dfnul3  4291  abf  4360  dfif2  4483  dfsn2ALT  4604  rabsnifsb  4681  tprot  4708  pw0  4770  pwpw0  4771  dfopif  4828  pwsn  4858  dfuni2  4867  dfint2  4906  dfiunv2  4991  cbviun  4992  cbviin  4993  cbviung  4994  cbviing  4995  cbviunv  4996  cbviinv  4997  iunrab  5010  viin  5022  iunsn  5023  iinuni  5055  cbvopab  5172  cbvopabv  5173  cbvopab1  5174  cbvopab1g  5175  cbvopab2  5176  cbvopab1s  5177  cbvopab1v  5178  cbvopab2v  5179  unopab  5180  zfrep4  5240  zfpair  5368  iunopab  5515  dfid2  5529  dfid3  5530  rabxp  5680  csbxp  5733  dfdm3  5844  dfrn2  5845  dfrn3  5846  dfdm4  5852  dfdmf  5853  csbdm  5854  dmun  5867  dmopab  5872  dmopabss  5875  dmopab3  5876  dfrnf  5907  rnopab  5911  rnopabss  5912  rnopab3  5913  rnmpt  5914  dfima2  6029  dfima3  6030  imadmrn  6037  imai  6041  args  6059  mptpreima  6204  dfiota2  6457  cbviotaw  6463  cbviotavw  6464  cbviota  6465  sb8iota  6467  mptfnf  6635  dffv4  6839  dfimafn2  6905  opabiotadm  6923  fndmin  6999  dffo3f  7060  fnasrn  7100  elabrex  7198  elabrexg  7199  abrexco  7200  dfoprab2  7426  cbvoprab2  7456  cbvoprab12v  7458  cbvoprab3v  7460  dmoprab  7471  rnoprab  7473  rnoprab2  7474  fnrnov  7541  abnex  7712  uniuni  7717  zfrep6  7909  fvresex  7914  abrexex2g  7918  abexssex  7924  abexex  7925  oprabrexex2  7932  dfopab2  8006  poseq  8110  soseq  8111  suppvalbr  8116  cnvimadfsn  8124  dfrecs3  8314  rdglem1  8356  snec  8727  pmex  8780  fset0  8803  f1setex  8806  0map0sn0  8835  dfixp  8849  cbvixp  8864  cbvixpv  8865  pwfir  9229  marypha2lem4  9353  tcsni  9662  scottexs  9811  scott0s  9812  kardex  9818  cardf2  9867  dfac3  10043  infmap2  10139  cf0  10173  cfval2  10182  isf33lem  10288  dffin1-5  10310  axdc2lem  10370  addcompr  10944  mulcompr  10946  dfnn3  12171  hashf1lem2  14391  prprrab  14408  cshwsexa  14759  trclun  14949  shftdm  15006  hashbc0  16945  lubfval  18283  glbfval  18296  odulub  18340  oduglb  18342  symgbas0  19330  symgsubmefmnd  19339  pmtrprfvalrn  19429  efgval2  19665  dvdsrval  20309  dfrhm2  20422  toponsspwpw  22878  tgval2  22912  tgdif0  22948  xkobval  23542  ustfn  24158  ustn0  24177  2lgslem1b  27371  2sq  27409  madeval2  27841  addsasslem1  28011  addsasslem2  28012  negsid  28049  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  twocut  28431  pw2cut2  28470  rusgrprc  29676  rgrprcx  29678  wwlksnfi  29991  clwwlkvbij  30200  dfconngr1  30275  isconngr  30276  isconngr1  30277  nmopnegi  32053  nmop0  32074  nmfn0  32075  sa-abvi  32531  dmrab  32583  abrexdomjm  32594  abrexexd  32596  cbviunf  32642  dfimafnf  32726  ofpreima  32755  intimafv  32801  maprnin  32821  fpwrelmapffslem  32822  hasheuni  34263  sigaex  34288  sigaval  34289  eulerpartlemt  34549  bnj1146  34967  bnj1400  35011  bnj882  35102  bnj893  35104  dfacycgr1  35360  derang0  35385  subfaclefac  35392  satfdm  35585  fmla0  35598  fmlasuc0  35600  fmla1  35603  dfon2lem7  36003  dfon2  36006  dfrdg2  36009  dfiota3  36137  fvline  36360  ellines  36368  sbceqbii  36407  rabeqbii  36410  iuneq12i  36411  iineq1i  36412  iineq12i  36413  ixpeq1i  36416  cbvcsbvw2  36447  cbviunvw2  36448  cbviinvw2  36449  cbvoprab1vw  36453  cbvoprab2vw  36454  cbvoprab123vw  36455  cbvoprab23vw  36456  cbvoprab13vw  36457  cbvixpvw2  36461  bj-dfnul2  36795  bj-df-ifc  36805  bj-dfif  36806  bj-rababw  37129  bj-inrab  37175  bj-taginv  37234  bj-nuliotaALT  37306  bj-dfid2ALT  37313  rnmptsn  37590  dissneqlem  37595  dissneq  37596  dffinxpf  37640  rabiun  37844  ismblfin  37912  volsupnfl  37916  areacirclem5  37963  abrexdom  37981  sdclem1  37994  sdc  37995  rncnvepres  38560  qsresid  38582  dmxrn  38638  dmcnvep  38639  rnxrn  38672  dfsuccl3  38724  dfsuccl4  38725  rncossdmcoss  38796  dfcoeleqvrels  38956  mpets  39207  psubspset  40120  pmapglb  40146  polval2N  40282  psubclsetN  40312  tendoset  41135  sticksstones16  42532  sticksstones21  42537  imaopab  42603  prjspeclsp  42970  sn-isghm  43031  eq0rabdioph  43133  rexrabdioph  43151  eldioph4b  43168  hbtlem6  43486  onsucrn  43628  dfno2  43784  alephiso2  43914  dfid7  43968  clcnvlem  43979  dfrtrcl5  43985  relopabVD  45256  iuneq1i  45444  dfaiota2  47446  dfaimafn2  47526  fundcmpsurinj  47769  fundcmpsurbijinj  47770  sprid  47834  stgr1  48321  setrec2  50054