Theorem abbii 2801

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993.) Remove dependency on ax-10 2137, ax-11 2154, and ax-12 2171. (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 1799	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

Syntax hints:   ↔ wb 205   = wceq 1541  {cab 2708

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723

This theorem is referenced by:  rabbiiaOLD  3410  rabrab  3428  dfv2  3449  rabab  3474  csb2  3860  cbvcsbw  3868  cbvcsb  3869  csbid  3871  csbcow  3873  csbco  3874  csbconstg  3877  csbie  3894  cbvreucsf  3905  ss2abdv  4025  unabw  4262  notabw  4268  unrab  4270  inrab  4271  inrab2  4272  difrab  4273  rabun2  4278  dfnul4  4289  dfnul2  4290  dfnul3  4291  dfnul2OLD  4292  dfnul3OLD  4293  dfnul4OLD  4294  abf  4367  dfif2  4493  dfsn2ALT  4611  rabsnifsb  4688  tprot  4715  pw0  4777  pwpw0  4778  dfopif  4832  pwsn  4862  pwsnOLD  4863  dfuni2  4872  uniprOLD  4889  dfint2  4914  dfiunv2  5000  cbviun  5001  cbviin  5002  cbviung  5003  cbviing  5004  iunrab  5017  iunidOLD  5026  viin  5030  iunsn  5031  iinuni  5063  cbvopab  5182  cbvopabv  5183  cbvopab1  5185  cbvopab1g  5186  cbvopab2  5187  cbvopab1s  5188  cbvopab1v  5189  cbvopab2v  5191  unopab  5192  zfrep4  5258  zfpair  5381  iunopab  5521  iunopabOLD  5522  dfid2  5538  dfid3  5539  rabxp  5685  csbxp  5736  dfdm3  5848  dfrn2  5849  dfrn3  5850  dfdm4  5856  dfdmf  5857  csbdm  5858  dmun  5871  dmopab  5876  dmopabss  5879  dmopab3  5880  dfrnf  5910  rnopab  5914  rnmpt  5915  dfima2  6020  dfima3  6021  imadmrn  6028  imai  6031  args  6049  mptpreima  6195  dfiota2  6454  cbviotaw  6460  cbviotavw  6461  cbviota  6463  sb8iota  6465  mptfnf  6641  dffv4  6844  dfimafn2  6911  opabiotadm  6928  fndmin  7000  fnasrn  7096  elabrex  7195  abrexco  7196  dfoprab2  7420  cbvoprab2  7450  dmoprab  7463  rnoprab  7465  rnoprab2  7466  fnrnov  7532  abnex  7696  uniuni  7701  zfrep6  7892  fvresex  7897  abrexex2g  7902  abexssex  7908  abexex  7909  oprabrexex2  7916  dfopab2  7989  poseq  8095  soseq  8096  suppvalbr  8101  cnvimadfsn  8108  dfwrecsOLD  8249  dfrecs3  8323  dfrecs3OLD  8324  rdglem1  8366  snec  8726  pmex  8777  fset0  8799  f1setex  8802  0map0sn0  8830  dfixp  8844  cbvixp  8859  pwfir  9127  marypha2lem4  9383  tcsni  9688  scottexs  9832  scott0s  9833  kardex  9839  cardf2  9888  dfac3  10066  infmap2  10163  cf0  10196  cfval2  10205  isf33lem  10311  dffin1-5  10333  axdc2lem  10393  addcompr  10966  mulcompr  10968  dfnn3  12176  hashf1lem2  14367  prprrab  14384  cshwsexa  14724  cshwsexaOLD  14725  trclun  14911  shftdm  14968  hashbc0  16888  lubfval  18253  glbfval  18266  odulub  18310  oduglb  18312  symgbas0  19184  symgsubmefmnd  19194  pmtrprfvalrn  19284  efgval2  19520  dvdsrval  20088  dfrhm2  20164  toponsspwpw  22308  tgval2  22343  tgdif0  22379  xkobval  22974  ustfn  23590  ustn0  23609  2lgslem1b  26777  2sq  26815  madeval2  27226  addsasslem1  27354  addsasslem2  27355  negsid  27382  rusgrprc  28601  rgrprcx  28603  wwlksnfi  28914  clwwlkvbij  29120  dfconngr1  29195  isconngr  29196  isconngr1  29197  nmopnegi  30970  nmop0  30991  nmfn0  30992  sa-abvi  31448  dmrab  31489  abrexdomjm  31497  abrexexd  31499  cbviunf  31541  dfimafnf  31617  ofpreima  31648  intimafv  31692  cnvoprabOLD  31705  maprnin  31716  fpwrelmapffslem  31717  hasheuni  32773  sigaex  32798  sigaval  32799  eulerpartlemt  33060  bnj1146  33492  bnj1400  33536  bnj882  33627  bnj893  33629  dfacycgr1  33825  derang0  33850  subfaclefac  33857  satfdm  34050  fmla0  34063  fmlasuc0  34065  fmla1  34068  dfon2lem7  34450  dfon2  34453  dfrdg2  34456  dfiota3  34584  fvline  34805  ellines  34813  bj-df-ifc  35120  bj-dfif  35121  bj-rababw  35424  bj-inrab  35470  bj-taginv  35530  bj-nuliotaALT  35602  bj-dfid2ALT  35609  rnmptsn  35879  dissneqlem  35884  dissneq  35885  dffinxpf  35929  rabiun  36124  ismblfin  36192  volsupnfl  36196  areacirclem5  36243  abrexdom  36262  sdclem1  36275  sdc  36276  rncnvepres  36837  qsresid  36859  rnxrn  36933  rncossdmcoss  36990  dfcoeleqvrels  37156  mpets  37377  psubspset  38280  pmapglb  38306  polval2N  38442  psubclsetN  38472  tendoset  39295  sticksstones16  40643  sticksstones21  40648  imaopab  40727  prjspeclsp  41008  eq0rabdioph  41157  rexrabdioph  41175  eldioph4b  41192  hbtlem6  41514  onsucrn  41664  dfno2  41822  alephiso2  41952  dfid7  42006  clcnvlem  42017  dfrtrcl5  42023  relopabVD  43305  elabrexg  43371  dffo3f  43520  dfaiota2  45438  dfaimafn2  45518  fundcmpsurinj  45721  fundcmpsurbijinj  45722  sprid  45786  setrec2  47260