Theorem abbii 2809

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

Syntax hints:   ↔ wb 205   = wceq 1539  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730

This theorem is referenced by:  rabrab  3305  rabbiia  3396  dfv2  3425  rabab  3450  csb2  3830  cbvcsbw  3838  cbvcsb  3839  csbid  3841  csbcow  3843  csbco  3844  csbconstg  3847  csbie  3864  cbvreucsf  3875  ss2abdv  3993  unabw  4228  notabw  4234  unrab  4236  inrab  4237  inrab2  4238  difrab  4239  rabun2  4244  dfnul4  4255  dfnul2  4256  dfnul3  4257  dfnul2OLD  4258  dfnul3OLD  4259  dfnul4OLD  4260  abf  4333  dfif2  4458  dfsn2ALT  4578  rabsnifsb  4655  tprot  4682  pw0  4742  pwpw0  4743  dfopifOLD  4798  pwsn  4828  pwsnOLD  4829  dfuni2  4838  uniprOLD  4855  dfint2  4878  dfiunv2  4961  cbviun  4962  cbviin  4963  cbviung  4964  cbviing  4965  iunrab  4978  iunid  4986  viin  4990  iunsn  4991  iinuni  5023  cbvopab  5142  cbvopabv  5143  cbvopab1  5145  cbvopab1g  5146  cbvopab2  5147  cbvopab1s  5148  cbvopab1v  5149  cbvopab2v  5151  unopab  5152  zfrep4  5215  zfpair  5339  iunopab  5465  dfid2  5482  dfid3  5483  rabxp  5626  csbxp  5676  dfdm3  5785  dfrn2  5786  dfrn3  5787  dfdm4  5793  dfdmf  5794  csbdm  5795  dmun  5808  dmopab  5813  dmopabss  5816  dmopab3  5817  domepOLD  5822  dfrnf  5848  rnopab  5852  rnmpt  5853  dfima2  5960  dfima3  5961  imadmrn  5968  imai  5971  args  5989  mptpreima  6130  dfiota2  6377  cbviotaw  6383  cbviotavw  6384  cbviota  6386  sb8iota  6388  mptfnf  6552  dffv4  6753  dfimafn2  6815  opabiotadm  6832  fndmin  6904  fnasrn  6999  elabrex  7098  abrexco  7099  dfoprab2  7311  cbvoprab2  7341  dmoprab  7354  rnoprab  7356  rnoprab2  7357  fnrnov  7423  abnex  7585  uniuni  7590  zfrep6  7771  fvresex  7776  abrexex2g  7780  abexssex  7786  abexex  7787  oprabrexex2  7794  dfopab2  7865  suppvalbr  7952  cnvimadfsn  7959  dfwrecsOLD  8100  dfrecs3  8174  dfrecs3OLD  8175  rdglem1  8217  snec  8527  pmex  8578  fset0  8600  f1setex  8603  0map0sn0  8631  dfixp  8645  cbvixp  8660  pwfir  8921  marypha2lem4  9127  tcsni  9432  scottexs  9576  scott0s  9577  kardex  9583  cardf2  9632  dfac3  9808  infmap2  9905  cf0  9938  cfval2  9947  isf33lem  10053  dffin1-5  10075  axdc2lem  10135  addcompr  10708  mulcompr  10710  dfnn3  11917  hashf1lem2  14098  prprrab  14115  cshwsexa  14465  trclun  14653  shftdm  14710  hashbc0  16634  lubfval  17983  glbfval  17996  odulub  18040  oduglb  18042  symgbas0  18911  symgsubmefmnd  18921  pmtrprfvalrn  19011  efgval2  19245  dvdsrval  19802  dfrhm2  19876  toponsspwpw  21979  tgval2  22014  tgdif0  22050  xkobval  22645  ustfn  23261  ustn0  23280  2lgslem1b  26445  2sq  26483  rusgrprc  27860  rgrprcx  27862  wwlksnfi  28172  clwwlkvbij  28378  dfconngr1  28453  isconngr  28454  isconngr1  28455  nmopnegi  30228  nmop0  30249  nmfn0  30250  sa-abvi  30706  dmrab  30745  abrexdomjm  30753  abrexexd  30755  cbviunf  30796  dfimafnf  30872  ofpreima  30904  intimafv  30945  cnvoprabOLD  30957  maprnin  30968  fpwrelmapffslem  30969  hasheuni  31953  sigaex  31978  sigaval  31979  eulerpartlemt  32238  bnj1146  32671  bnj1400  32715  bnj882  32806  bnj893  32808  dfacycgr1  33006  derang0  33031  subfaclefac  33038  satfdm  33231  fmla0  33244  fmlasuc0  33246  fmla1  33249  dfon2lem7  33671  dfon2  33674  dfrdg2  33677  poseq  33729  soseq  33730  madeval2  33964  dfiota3  34152  fvline  34373  ellines  34381  bj-df-ifc  34688  bj-dfif  34689  bj-rababw  34993  bj-inrab  35042  bj-taginv  35103  bj-nuliotaALT  35156  bj-dfid2ALT  35163  rnmptsn  35433  dissneqlem  35438  dissneq  35439  dffinxpf  35483  rabiun  35677  ismblfin  35745  volsupnfl  35749  areacirclem5  35796  abrexdom  35815  sdclem1  35828  sdc  35829  rncnvepres  36366  qsresid  36387  rnxrn  36451  rncossdmcoss  36500  dfcoeleqvrels  36661  psubspset  37685  pmapglb  37711  polval2N  37847  psubclsetN  37877  tendoset  38700  sticksstones16  40046  sticksstones21  40051  imaopab  40133  prjspeclsp  40372  eq0rabdioph  40514  rexrabdioph  40532  eldioph4b  40549  hbtlem6  40870  alephiso2  41054  dfid7  41109  clcnvlem  41120  dfrtrcl5  41126  relopabVD  42410  elabrexg  42478  dffo3f  42606  dfaiota2  44465  dfaimafn2  44545  fundcmpsurinj  44749  fundcmpsurbijinj  44750  sprid  44814  setrec2  46287