Theorem abbii 2803

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 2184. (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 2801	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})
2		abbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1798	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

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

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 2708

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

This theorem is referenced by:  rabrab  3423  dfv2  3443  rabab  3471  csb2  3851  cbvcsbw  3859  cbvcsb  3860  cbvcsbv  3861  csbid  3862  csbcow  3864  csbco  3865  csbconstg  3868  csbie  3884  cbvreucsf  3893  unabw  4259  notabw  4265  unrab  4267  inrab  4268  inrab2  4269  difrab  4270  rabun2  4276  dfnul4  4287  dfnul2  4288  dfnul3  4289  abf  4358  dfif2  4481  dfsn2ALT  4602  rabsnifsb  4679  tprot  4706  pw0  4768  pwpw0  4769  dfopif  4826  pwsn  4856  dfuni2  4865  dfint2  4904  dfiunv2  4989  cbviun  4990  cbviin  4991  cbviung  4992  cbviing  4993  cbviunv  4994  cbviinv  4995  iunrab  5008  viin  5020  iunsn  5021  iinuni  5053  cbvopab  5170  cbvopabv  5171  cbvopab1  5172  cbvopab1g  5173  cbvopab2  5174  cbvopab1s  5175  cbvopab1v  5176  cbvopab2v  5177  unopab  5178  zfrep4  5238  zfpair  5366  iunopab  5507  dfid2  5521  dfid3  5522  rabxp  5672  csbxp  5725  dfdm3  5836  dfrn2  5837  dfrn3  5838  dfdm4  5844  dfdmf  5845  csbdm  5846  dmun  5859  dmopab  5864  dmopabss  5867  dmopab3  5868  dfrnf  5899  rnopab  5903  rnopabss  5904  rnopab3  5905  rnmpt  5906  dfima2  6021  dfima3  6022  imadmrn  6029  imai  6033  args  6051  mptpreima  6196  dfiota2  6449  cbviotaw  6455  cbviotavw  6456  cbviota  6457  sb8iota  6459  mptfnf  6627  dffv4  6831  dfimafn2  6897  opabiotadm  6915  fndmin  6990  dffo3f  7051  fnasrn  7090  elabrex  7188  elabrexg  7189  abrexco  7190  dfoprab2  7416  cbvoprab2  7446  cbvoprab12v  7448  cbvoprab3v  7450  dmoprab  7461  rnoprab  7463  rnoprab2  7464  fnrnov  7531  abnex  7702  uniuni  7707  zfrep6  7899  fvresex  7904  abrexex2g  7908  abexssex  7914  abexex  7915  oprabrexex2  7922  dfopab2  7996  poseq  8100  soseq  8101  suppvalbr  8106  cnvimadfsn  8114  dfrecs3  8304  rdglem1  8346  snec  8715  pmex  8768  fset0  8791  f1setex  8794  0map0sn0  8823  dfixp  8837  cbvixp  8852  cbvixpv  8853  pwfir  9217  marypha2lem4  9341  tcsni  9650  scottexs  9799  scott0s  9800  kardex  9806  cardf2  9855  dfac3  10031  infmap2  10127  cf0  10161  cfval2  10170  isf33lem  10276  dffin1-5  10298  axdc2lem  10358  addcompr  10932  mulcompr  10934  dfnn3  12159  hashf1lem2  14379  prprrab  14396  cshwsexa  14747  trclun  14937  shftdm  14994  hashbc0  16933  lubfval  18271  glbfval  18284  odulub  18328  oduglb  18330  symgbas0  19318  symgsubmefmnd  19327  pmtrprfvalrn  19417  efgval2  19653  dvdsrval  20297  dfrhm2  20410  toponsspwpw  22866  tgval2  22900  tgdif0  22936  xkobval  23530  ustfn  24146  ustn0  24165  2lgslem1b  27359  2sq  27397  madeval2  27829  addsasslem1  27999  addsasslem2  28000  negsid  28037  addsdilem1  28147  addsdilem2  28148  mulsasslem1  28159  mulsasslem2  28160  twocut  28419  pw2cut2  28458  rusgrprc  29664  rgrprcx  29666  wwlksnfi  29979  clwwlkvbij  30188  dfconngr1  30263  isconngr  30264  isconngr1  30265  nmopnegi  32040  nmop0  32061  nmfn0  32062  sa-abvi  32518  dmrab  32571  abrexdomjm  32582  abrexexd  32584  cbviunf  32630  dfimafnf  32714  ofpreima  32743  intimafv  32790  maprnin  32810  fpwrelmapffslem  32811  hasheuni  34242  sigaex  34267  sigaval  34268  eulerpartlemt  34528  bnj1146  34947  bnj1400  34991  bnj882  35082  bnj893  35084  dfacycgr1  35338  derang0  35363  subfaclefac  35370  satfdm  35563  fmla0  35576  fmlasuc0  35578  fmla1  35581  dfon2lem7  35981  dfon2  35984  dfrdg2  35987  dfiota3  36115  fvline  36338  ellines  36346  sbceqbii  36385  rabeqbii  36388  iuneq12i  36389  iineq1i  36390  iineq12i  36391  ixpeq1i  36394  cbvcsbvw2  36425  cbviunvw2  36426  cbviinvw2  36427  cbvoprab1vw  36431  cbvoprab2vw  36432  cbvoprab123vw  36433  cbvoprab23vw  36434  cbvoprab13vw  36435  cbvixpvw2  36439  bj-df-ifc  36780  bj-dfif  36781  bj-rababw  37082  bj-inrab  37128  bj-taginv  37187  bj-nuliotaALT  37259  bj-dfid2ALT  37266  rnmptsn  37540  dissneqlem  37545  dissneq  37546  dffinxpf  37590  rabiun  37794  ismblfin  37862  volsupnfl  37866  areacirclem5  37913  abrexdom  37931  sdclem1  37944  sdc  37945  rncnvepres  38502  qsresid  38524  dmxrn  38572  dmcnvep  38573  rnxrn  38606  dfsuccl3  38647  dfsuccl4  38648  rncossdmcoss  38718  dfcoeleqvrels  38878  mpets  39101  psubspset  40004  pmapglb  40030  polval2N  40166  psubclsetN  40196  tendoset  41019  sticksstones16  42416  sticksstones21  42421  imaopab  42487  prjspeclsp  42855  sn-isghm  42916  eq0rabdioph  43018  rexrabdioph  43036  eldioph4b  43053  hbtlem6  43371  onsucrn  43513  dfno2  43669  alephiso2  43799  dfid7  43853  clcnvlem  43864  dfrtrcl5  43870  relopabVD  45141  iuneq1i  45329  dfaiota2  47332  dfaimafn2  47412  fundcmpsurinj  47655  fundcmpsurbijinj  47656  sprid  47720  stgr1  48207  setrec2  49940