Theorem abbii 2829

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

Syntax hints:   ↔ wb 208   = wceq 1560  {cab 2740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754

This theorem is referenced by:  dfv2  3457  rabab  3484  csb2  3854  cbvcsbw  3862  cbvcsb  3863  cbvcsbv  3864  csbid  3865  csbcow  3867  csbco  3868  csbconstg  3871  csbie  3887  cbvreucsf  3896  unabw  4259  notabw  4265  unrab  4267  inrab  4268  inrab2  4269  difrab  4270  rabun2  4276  dfnul4  4287  dfnul2  4288  dfnul3  4289  abf  4360  dfif2  4482  dfsn2ALT  4604  rabsnifsb  4681  tprot  4708  pw0  4770  pwpw0  4771  dfopif  4828  pwsn  4858  dfuni2  4867  dfint2  4907  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  5243  zfpair  5378  iunopab  5530  dfid2  5544  dfid3  5545  rabxp  5695  csbxp  5748  dfdm3  5863  dfrn2  5864  dfrn3  5865  dfdm4  5871  dfdmf  5872  csbdm  5873  dmun  5886  dmopab  5891  dmopabss  5894  dmopab3  5895  dfrnf  5926  rnopab  5930  rnopabss  5931  rnopab3  5932  rnmpt  5933  dfima2  6051  dfima3  6052  imadmrn  6059  imai  6063  args  6081  mptpreima  6225  dfiota2  6478  cbviotaw  6484  cbviotavw  6485  cbviota  6486  sb8iota  6488  mptfnf  6656  dffv4  6864  dfimafn2  6930  opabiotadm  6948  fndmin  7026  dffo3f  7087  fnasrn  7127  elabrex  7226  elabrexg  7227  abrexco  7228  dfoprab2  7454  cbvoprab2  7484  cbvoprab12v  7486  cbvoprab3v  7488  dmoprab  7499  rnoprab  7501  rnoprab2  7502  fnrnov  7569  abnex  7740  uniuni  7745  zfrep6OLD  7936  fvresex  7941  abrexex2g  7945  abexssex  7951  abexex  7952  oprabrexex2  7959  dfopab2  8033  poseq  8138  soseq  8139  suppvalbr  8144  cnvimadfsn  8152  dfrecs3  8343  rdglem1  8386  snec  8760  pmex  8813  fset0  8835  f1setex  8838  0map0sn0  8867  dfixp  8881  cbvixp  8896  cbvixpv  8897  pwfir  9261  marypha2lem4  9384  tcsni  9696  scottexs  9845  scott0s  9846  kardex  9852  cardf2  9901  dfac3  10077  infmap2  10173  cf0  10207  cfval2  10217  isf33lem  10323  dffin1-5  10345  axdc2lem  10405  addcompr  10979  mulcompr  10981  dfnn3  12224  hashf1lem2  14469  prprrab  14486  cshwsexa  14837  trclun  15027  shftdm  15084  hashbc0  17041  lubfval  18380  glbfval  18393  odulub  18437  oduglb  18439  symgbas0  19429  symgsubmefmnd  19438  pmtrprfvalrn  19528  efgval2  19764  dvdsrval  20406  dfrhm2  20519  toponsspwpw  22979  tgval2  23013  tgdif0  23049  xkobval  23643  ustfn  24259  ustn0  24278  2lgslem1b  27453  2sq  27491  madeval2  27923  addsasslem1  28093  addsasslem2  28094  negsid  28131  addsdilem1  28241  addsdilem2  28242  mulsasslem1  28253  mulsasslem2  28254  twocut  28513  pw2cut2  28552  rusgrprc  29788  rgrprcx  29790  wwlksnfi  30103  clwwlkvbij  30312  dfconngr1  30387  isconngr  30388  isconngr1  30389  nmopnegi  32165  nmop0  32186  nmfn0  32187  sa-abvi  32643  dmrab  32693  abrexdomjm  32703  abrexexd  32705  cbviunf  32752  dfimafnf  32835  ofpreima  32864  intimafv  32910  maprnin  32930  fpwrelmapffslem  32931  hasheuni  34379  sigaex  34404  sigaval  34405  eulerpartlemt  34665  bnj1146  35083  bnj1400  35127  bnj882  35218  bnj893  35220  dfacycgr1  35491  derang0  35516  subfaclefac  35523  satfdm  35716  fmla0  35729  fmlasuc0  35731  fmla1  35734  dfon2lem7  36134  dfon2  36137  dfrdg2  36140  dfiota3  36268  fvline  36491  ellines  36499  sbceqbii  36548  rabeqbii  36551  iuneq12i  36552  iineq1i  36553  iineq12i  36554  ixpeq1i  36557  cbvcsbvw2  36588  cbviunvw2  36589  cbviinvw2  36590  cbvoprab1vw  36594  cbvoprab2vw  36595  cbvoprab123vw  36596  cbvoprab23vw  36597  cbvoprab13vw  36598  cbvixpvw2  36602  bj-dfnul2  37010  bj-df-ifc  37020  bj-dfif  37021  bj-rababw  37363  bj-inrab  37409  bj-taginv  37468  bj-nuliotaALT  37540  bj-dfid2ALT  37547  rnmptsn  37826  dissneqlem  37831  dissneq  37832  dffinxpf  37876  rabiun  38089  ismblfin  38157  volsupnfl  38161  areacirclem5  38208  abrexdom  38226  sdclem1  38239  sdc  38240  rncnvepres  38805  qsresid  38827  dmxrn  38883  dmcnvep  38884  rnxrn  38917  dfsuccl3  38969  dfsuccl4  38970  rncossdmcoss  39041  dfcoeleqvrels  39201  mpets  39452  psubspset  40365  pmapglb  40391  polval2N  40527  psubclsetN  40557  tendoset  41380  sticksstones16  42776  sticksstones21  42781  imaopab  42847  prjspeclsp  43191  sn-isghm  43252  eq0rabdioph  43354  rexrabdioph  43368  eldioph4b  43385  hbtlem6  43703  onsucrn  43845  dfno2  44001  alephiso2  44131  dfid7  44185  clcnvlem  44196  dfrtrcl5  44202  relopabVD  45473  iuneq1i  45661  dfaiota2  47677  dfaimafn2  47757  fundcmpsurinj  48012  fundcmpsurbijinj  48013  sprid  48077  stgr1  48580  setrec2  50313