Theorem abbii 2809

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731

This theorem is referenced by:  rabrab  3312  rabbiia  3408  dfv2  3436  rabab  3461  csb2  3835  cbvcsbw  3843  cbvcsb  3844  csbid  3846  csbcow  3848  csbco  3849  csbconstg  3852  csbie  3869  cbvreucsf  3880  ss2abdv  3998  unabw  4232  notabw  4238  unrab  4240  inrab  4241  inrab2  4242  difrab  4243  rabun2  4248  dfnul4  4259  dfnul2  4260  dfnul3  4261  dfnul2OLD  4262  dfnul3OLD  4263  dfnul4OLD  4264  abf  4337  dfif2  4462  dfsn2ALT  4582  rabsnifsb  4659  tprot  4686  pw0  4746  pwpw0  4747  dfopifOLD  4802  pwsn  4832  pwsnOLD  4833  dfuni2  4842  uniprOLD  4859  dfint2  4882  dfiunv2  4966  cbviun  4967  cbviin  4968  cbviung  4969  cbviing  4970  iunrab  4983  iunid  4991  viin  4995  iunsn  4996  iinuni  5028  cbvopab  5147  cbvopabv  5148  cbvopab1  5150  cbvopab1g  5151  cbvopab2  5152  cbvopab1s  5153  cbvopab1v  5154  cbvopab2v  5156  unopab  5157  zfrep4  5221  zfpair  5345  iunopab  5473  iunopabOLD  5474  dfid2  5492  dfid3  5493  rabxp  5636  csbxp  5687  dfdm3  5799  dfrn2  5800  dfrn3  5801  dfdm4  5807  dfdmf  5808  csbdm  5809  dmun  5822  dmopab  5827  dmopabss  5830  dmopab3  5831  domepOLD  5836  dfrnf  5862  rnopab  5866  rnmpt  5867  dfima2  5974  dfima3  5975  imadmrn  5982  imai  5985  args  6003  mptpreima  6146  dfiota2  6396  cbviotaw  6402  cbviotavw  6403  cbviota  6405  sb8iota  6407  mptfnf  6577  dffv4  6780  dfimafn2  6842  opabiotadm  6859  fndmin  6931  fnasrn  7026  elabrex  7125  abrexco  7126  dfoprab2  7342  cbvoprab2  7372  dmoprab  7385  rnoprab  7387  rnoprab2  7388  fnrnov  7454  abnex  7616  uniuni  7621  zfrep6  7806  fvresex  7811  abrexex2g  7816  abexssex  7822  abexex  7823  oprabrexex2  7830  dfopab2  7901  suppvalbr  7990  cnvimadfsn  7997  dfwrecsOLD  8138  dfrecs3  8212  dfrecs3OLD  8213  rdglem1  8255  snec  8578  pmex  8629  fset0  8651  f1setex  8654  0map0sn0  8682  dfixp  8696  cbvixp  8711  pwfir  8968  marypha2lem4  9206  tcsni  9510  scottexs  9654  scott0s  9655  kardex  9661  cardf2  9710  dfac3  9886  infmap2  9983  cf0  10016  cfval2  10025  isf33lem  10131  dffin1-5  10153  axdc2lem  10213  addcompr  10786  mulcompr  10788  dfnn3  11996  hashf1lem2  14179  prprrab  14196  cshwsexa  14546  trclun  14734  shftdm  14791  hashbc0  16715  lubfval  18077  glbfval  18090  odulub  18134  oduglb  18136  symgbas0  19005  symgsubmefmnd  19015  pmtrprfvalrn  19105  efgval2  19339  dvdsrval  19896  dfrhm2  19970  toponsspwpw  22080  tgval2  22115  tgdif0  22151  xkobval  22746  ustfn  23362  ustn0  23381  2lgslem1b  26549  2sq  26587  rusgrprc  27966  rgrprcx  27968  wwlksnfi  28280  clwwlkvbij  28486  dfconngr1  28561  isconngr  28562  isconngr1  28563  nmopnegi  30336  nmop0  30357  nmfn0  30358  sa-abvi  30814  dmrab  30853  abrexdomjm  30861  abrexexd  30863  cbviunf  30904  dfimafnf  30980  ofpreima  31011  intimafv  31052  cnvoprabOLD  31064  maprnin  31075  fpwrelmapffslem  31076  hasheuni  32062  sigaex  32087  sigaval  32088  eulerpartlemt  32347  bnj1146  32780  bnj1400  32824  bnj882  32915  bnj893  32917  dfacycgr1  33115  derang0  33140  subfaclefac  33147  satfdm  33340  fmla0  33353  fmlasuc0  33355  fmla1  33358  dfon2lem7  33774  dfon2  33777  dfrdg2  33780  poseq  33811  soseq  33812  madeval2  34046  dfiota3  34234  fvline  34455  ellines  34463  bj-df-ifc  34770  bj-dfif  34771  bj-rababw  35075  bj-inrab  35124  bj-taginv  35185  bj-nuliotaALT  35238  bj-dfid2ALT  35245  rnmptsn  35515  dissneqlem  35520  dissneq  35521  dffinxpf  35565  rabiun  35759  ismblfin  35827  volsupnfl  35831  areacirclem5  35878  abrexdom  35897  sdclem1  35910  sdc  35911  rncnvepres  36446  qsresid  36467  rnxrn  36531  rncossdmcoss  36580  dfcoeleqvrels  36741  psubspset  37765  pmapglb  37791  polval2N  37927  psubclsetN  37957  tendoset  38780  sticksstones16  40125  sticksstones21  40130  imaopab  40214  prjspeclsp  40458  eq0rabdioph  40605  rexrabdioph  40623  eldioph4b  40640  hbtlem6  40961  alephiso2  41172  dfid7  41227  clcnvlem  41238  dfrtrcl5  41244  relopabVD  42528  elabrexg  42596  dffo3f  42724  dfaiota2  44589  dfaimafn2  44669  fundcmpsurinj  44872  fundcmpsurbijinj  44873  sprid  44937  setrec2  46412