Theorem abbii 2827

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752

This theorem is used by:  dfv2  3453  rabab  3480  csb2  3849  cbvcsbw  3857  cbvcsb  3858  cbvcsbv  3859  csbid  3860  csbcow  3862  csbco  3863  csbconstg  3866  csbie  3882  cbvreucsf  3891  unabw  4253  notabw  4259  unrab  4261  inrab  4262  inrab2  4263  difrab  4264  rabun2  4270  dfnul4  4281  dfnul2  4282  dfnul3  4283  abf  4364  dfif2  4484  dfsn2ALT  4606  rabsnifsb  4683  tprot  4710  pw0  4773  pwpw0  4774  dfopif  4830  pwsn  4860  dfuni2  4869  dfint2  4909  dfiunv2  4992  cbviun  4993  cbviin  4994  cbviung  4995  cbviing  4996  cbviunv  4997  cbviinv  4998  iunrab  5011  viin  5023  iunsn  5024  iinuni  5058  cbvopab  5177  cbvopabv  5178  cbvopab1  5179  cbvopab1g  5180  cbvopab2  5181  cbvopab1s  5182  cbvopab1v  5183  cbvopab2v  5184  unopab  5185  zfrep4  5248  zfpair  5386  iunopab  5538  dfid2  5552  dfid3  5553  rabxp  5703  csbxp  5756  dfdm3  5871  dfrn2  5872  dfrn3  5873  dfdm4  5879  dfdmf  5880  csbdm  5881  dmun  5894  dmopab  5899  dmopabss  5902  dmopab3  5903  dfrnf  5934  rnopab  5938  rnopabss  5939  rnopab3  5940  rnmpt  5941  dfima2  6058  dfima3  6059  imadmrn  6066  imai  6070  args  6088  mptpreima  6234  dfiota2  6490  cbviotaw  6496  cbviotavw  6497  cbviota  6498  sb8iota  6500  mptfnf  6667  dffv4  6875  dfimafn2  6941  opabiotadm  6959  fndmin  7037  dffo3f  7099  fnasrn  7141  elabrex  7239  elabrexg  7240  abrexco  7241  dfoprab2  7471  cbvoprab2  7501  cbvoprab12v  7503  cbvoprab3v  7505  dmoprab  7516  rnoprab  7518  rnoprab2  7519  fnrnov  7587  abnex  7756  uniuni  7761  zfrep6OLD  7952  fvresex  7957  abrexex2g  7961  abexssex  7967  abexex  7968  oprabrexex2  7975  dfopab2  8049  poseq  8156  soseq  8157  suppvalbr  8162  cnvimadfsn  8170  dfrecs3  8361  rdglem1  8404  snec  8778  pmex  8831  fset0  8855  f1setex  8858  0map0sn0  8892  dfixp  8906  cbvixp  8921  cbvixpv  8922  pwfir  9286  marypha2lem4  9408  tcsni  9720  scottexsOLD  9882  scott0bsOLD  9884  kardexOLD  9897  cardf2  9948  dfac3  10124  infmap2  10219  cf0  10252  cfval2  10262  isf33lem  10368  dffin1-5  10390  axdc2lem  10450  addcompr  11030  mulcompr  11032  dfnn3  12271  hashf1lem2  14521  prprrab  14538  cshwsexa  14895  trclun  15087  shftdm  15144  hashbc0  17097  lubfval  18436  glbfval  18449  odulub  18493  oduglb  18495  symgbas0  19516  symgsubmefmnd  19525  pmtrprfvalrn  19615  efgval2  19851  dvdsrval  20502  dfrhm2  20615  toponsspwpw  23147  tgval2  23181  tgdif0  23217  xkobval  23812  ustfn  24428  ustn0  24447  2lgslem1b  27628  2sq  27666  madeval2  28098  addsasslem1  28268  addsasslem2  28269  negsid  28306  addsdilem1  28416  addsdilem2  28417  mulsasslem1  28428  mulsasslem2  28429  twocut  28688  pw2cut2  28727  rusgrprc  30050  rgrprcx  30052  wwlksnfi  30374  clwwlkvbij  30583  dfacycgr1  30629  dfconngr1  30668  isconngr  30669  isconngr1  30670  nmopnegi  32446  nmop0  32467  nmfn0  32468  sa-abvi  32924  dmrab  32972  abrexdomjm  32982  abrexexd  32984  cbviunf  33029  dfimafnf  33109  ofpreima  33138  intimafv  33183  maprnin  33202  fpwrelmapffslem  33203  hasheuni  34595  sigaex  34620  sigaval  34621  eulerpartlemt  34882  bnj1146  35300  bnj1400  35344  bnj882  35435  bnj893  35437  derang0  35748  subfaclefac  35755  satfdm  35948  fmla0  35961  fmlasuc0  35963  fmla1  35966  dfon2lem7  36366  dfon2  36369  dfrdg2  36372  dfiota3  36500  fvline  36724  ellines  36732  sbceqbii  36811  rabeqbii  36814  iuneq12i  36815  iineq1i  36816  iineq12i  36817  ixpeq1i  36820  cbvcsbvw2  36851  cbviunvw2  36852  cbviinvw2  36853  cbvoprab1vw  36857  cbvoprab2vw  36858  cbvoprab123vw  36859  cbvoprab23vw  36860  cbvoprab13vw  36861  cbvixpvw2  36865  bj-dfnul2  37271  bj-df-ifc  37281  bj-dfif  37282  bj-rababw  37624  bj-inrab  37671  bj-taginv  37730  bj-nuliotaALT  37802  bj-dfid2ALT  37809  rnmptsn  38089  dissneqlem  38094  dissneq  38095  dffinxpf  38139  rabiun  38352  ismblfin  38410  volsupnfl  38414  areacirclem5  38461  abrexdom  38480  sdclem1  38493  sdc  38494  rncnvepres  39057  qsresid  39079  dmxrn  39135  dmcnvep  39136  rnxrn  39169  dfsuccl3  39221  dfsuccl4  39222  rncossdmcoss  39293  dfcoeleqvrels  39453  mpets  39704  psubspset  40617  pmapglb  40643  polval2N  40779  psubclsetN  40809  tendoset  41632  sticksstones16  43028  sticksstones21  43033  imaopab  43101  prjspeclsp  43458  sn-isghm  43519  eq0rabdioph  43621  rexrabdioph  43635  eldioph4b  43652  hbtlem6  43970  onsucrn  44112  dfno2  44268  alephiso2  44398  dfid7  44452  clcnvlem  44463  dfrtrcl5  44469  relopabVD  45723  iuneq1i  45918  dfaiota2  47974  dfaimafn2  48054  fundcmpsurinj  48309  fundcmpsurbijinj  48310  sprid  48374  stgr1  48877  setrec2  50621