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 1826	1 ⊢ {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓}

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  {cab 2740

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754

This theorem is used 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  4370  dfif2  4488  dfsn2ALT  4610  rabsnifsb  4687  tprot  4714  pw0  4777  pwpw0  4778  dfopif  4834  pwsn  4864  dfuni2  4873  dfint2  4913  dfiunv2  4997  cbviun  4998  cbviin  4999  cbviung  5000  cbviing  5001  cbviunv  5002  cbviinv  5003  iunrab  5016  viin  5028  iunsn  5029  iinuni  5063  cbvopab  5182  cbvopabv  5183  cbvopab1  5184  cbvopab1g  5185  cbvopab2  5186  cbvopab1s  5187  cbvopab1v  5188  cbvopab2v  5189  unopab  5190  zfrep4  5253  zfpair  5391  iunopab  5543  dfid2  5557  dfid3  5558  rabxp  5708  csbxp  5761  dfdm3  5876  dfrn2  5877  dfrn3  5878  dfdm4  5884  dfdmf  5885  csbdm  5886  dmun  5899  dmopab  5904  dmopabss  5907  dmopab3  5908  dfrnf  5939  rnopab  5943  rnopabss  5944  rnopab3  5945  rnmpt  5946  dfima2  6063  dfima3  6064  imadmrn  6071  imai  6075  args  6093  mptpreima  6238  dfiota2  6493  cbviotaw  6499  cbviotavw  6500  cbviota  6501  sb8iota  6503  mptfnf  6670  dffv4  6878  dfimafn2  6944  opabiotadm  6962  fndmin  7040  dffo3f  7101  fnasrn  7141  elabrex  7240  elabrexg  7241  abrexco  7242  dfoprab2  7470  cbvoprab2  7500  cbvoprab12v  7502  cbvoprab3v  7504  dmoprab  7515  rnoprab  7517  rnoprab2  7518  fnrnov  7585  abnex  7754  uniuni  7759  zfrep6OLD  7950  fvresex  7955  abrexex2g  7959  abexssex  7965  abexex  7966  oprabrexex2  7973  dfopab2  8047  poseq  8152  soseq  8153  suppvalbr  8158  cnvimadfsn  8166  dfrecs3  8357  rdglem1  8400  snec  8774  pmex  8827  fset0  8849  f1setex  8852  0map0sn0  8881  dfixp  8895  cbvixp  8910  cbvixpv  8911  pwfir  9274  marypha2lem4  9396  tcsni  9708  scottexsOLD  9870  scott0bsOLD  9872  kardexOLD  9885  cardf2  9936  dfac3  10112  infmap2  10207  cf0  10240  cfval2  10250  isf33lem  10356  dffin1-5  10378  axdc2lem  10438  addcompr  11012  mulcompr  11014  dfnn3  12253  hashf1lem2  14500  prprrab  14517  cshwsexa  14868  trclun  15058  shftdm  15115  hashbc0  17071  lubfval  18410  glbfval  18423  odulub  18467  oduglb  18469  symgbas0  19465  symgsubmefmnd  19474  pmtrprfvalrn  19564  efgval2  19800  dvdsrval  20450  dfrhm2  20563  toponsspwpw  23090  tgval2  23124  tgdif0  23160  xkobval  23754  ustfn  24370  ustn0  24389  2lgslem1b  27567  2sq  27605  madeval2  28037  addsasslem1  28207  addsasslem2  28208  negsid  28245  addsdilem1  28355  addsdilem2  28356  mulsasslem1  28367  mulsasslem2  28368  twocut  28627  pw2cut2  28666  rusgrprc  29951  rgrprcx  29953  wwlksnfi  30266  clwwlkvbij  30475  dfconngr1  30550  isconngr  30551  isconngr1  30552  nmopnegi  32328  nmop0  32349  nmfn0  32350  sa-abvi  32806  dmrab  32854  abrexdomjm  32864  abrexexd  32866  cbviunf  32911  dfimafnf  32992  ofpreima  33021  intimafv  33067  maprnin  33087  fpwrelmapffslem  33088  hasheuni  34484  sigaex  34509  sigaval  34510  eulerpartlemt  34770  bnj1146  35188  bnj1400  35232  bnj882  35323  bnj893  35325  dfacycgr1  35644  derang0  35669  subfaclefac  35676  satfdm  35869  fmla0  35882  fmlasuc0  35884  fmla1  35887  dfon2lem7  36287  dfon2  36290  dfrdg2  36293  dfiota3  36421  fvline  36644  ellines  36652  sbceqbii  36731  rabeqbii  36734  iuneq12i  36735  iineq1i  36736  iineq12i  36737  ixpeq1i  36740  cbvcsbvw2  36771  cbviunvw2  36772  cbviinvw2  36773  cbvoprab1vw  36777  cbvoprab2vw  36778  cbvoprab123vw  36779  cbvoprab23vw  36780  cbvoprab13vw  36781  cbvixpvw2  36785  bj-dfnul2  37191  bj-df-ifc  37201  bj-dfif  37202  bj-rababw  37544  bj-inrab  37591  bj-taginv  37650  bj-nuliotaALT  37722  bj-dfid2ALT  37729  rnmptsn  38009  dissneqlem  38014  dissneq  38015  dffinxpf  38059  rabiun  38272  ismblfin  38340  volsupnfl  38344  areacirclem5  38391  abrexdom  38409  sdclem1  38422  sdc  38423  rncnvepres  38986  qsresid  39008  dmxrn  39064  dmcnvep  39065  rnxrn  39098  dfsuccl3  39150  dfsuccl4  39151  rncossdmcoss  39222  dfcoeleqvrels  39382  mpets  39633  psubspset  40546  pmapglb  40572  polval2N  40708  psubclsetN  40738  tendoset  41561  sticksstones16  42957  sticksstones21  42962  imaopab  43030  prjspeclsp  43372  sn-isghm  43433  eq0rabdioph  43535  rexrabdioph  43549  eldioph4b  43566  hbtlem6  43884  onsucrn  44026  dfno2  44182  alephiso2  44312  dfid7  44366  clcnvlem  44377  dfrtrcl5  44383  relopabVD  45637  iuneq1i  45832  dfaiota2  47851  dfaimafn2  47931  fundcmpsurinj  48186  fundcmpsurbijinj  48187  sprid  48251  stgr1  48754  setrec2  50501