Theorem abbidv 2802

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2172, based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.)

Hypothesis

Ref	Expression
abbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
abbidv	⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem abbidv

Step	Hyp	Ref	Expression
1		abbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	alrimiv 1931	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		abbi 2801	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
4	2, 3	syl 17	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540   = wceq 1542  {cab 2710

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725

This theorem is referenced by:  rabbidva2  3435  cdeqab  3767  sbceqbid  3785  csbeq1  3897  csbeq2  3899  csbeq2d  3900  csbprc  4407  sbcel12  4409  sbceqg  4410  csbnestgfw  4420  csbnestgf  4425  pweqALT  4618  sneq  4639  csbsng  4713  unieqOLD  4921  uniprg  4926  csbuni  4941  inteq  4954  iineq1  5015  iineq2  5018  dfiin2g  5036  iinrab  5073  iinxprg  5093  opabbid  5214  opabbidv  5215  axrep6g  5294  imasng  6083  predres  6341  iotaeq  6509  iotabi  6510  dfimafn  6955  fnsnfvOLD  6972  fliftf  7312  oprabbid  7474  oprabbidv  7475  frecseq123  8267  csbfrecsg  8269  wrecseq123OLD  8300  rdglim2  8432  qseq1  8757  qseq2  8758  qsinxp  8787  mapvalg  8830  fsetexb  8858  ixpsnval  8894  ixpeq1  8902  fival  9407  tcvalg  9733  karden  9890  acneq  10038  infmap2  10213  cfval  10242  cflim3  10257  axdclem  10514  axdc  10516  rankcf  10772  genpv  10994  negfi  12163  supadd  12182  hashf1lem2  14417  hashf1  14418  hashfac  14419  csbwrdg  14494  cshimadifsn  14780  cshimadifsn0  14781  cleq1  14930  dfrtrcl2  15009  shftlem  15015  shftfib  15019  vdwlem6  16919  cshwsiun  17033  lubfval  18303  glbfval  18316  eqglact  19059  qus0subgbas  19075  isghm  19092  symgval  19236  sylow1lem2  19467  sylow3lem1  19495  efgval  19585  dmdprd  19868  ixpsnbasval  20832  cssval  21235  aspval2  21452  ressmplbas2  21582  tgval  22458  clsval2  22554  lpfval  22642  lpval  22643  islocfin  23021  ptval  23074  hauspwpwf1  23491  ptcmplem2  23557  snclseqg  23620  ustval  23707  itg2val  25246  limcfval  25389  plyval  25707  addsval  27446  addscom  27450  addsass  27488  mulsval  27565  mulscom  27595  addsdi  27610  mulsass  27621  precsexlemcbv  27652  precsexlem3  27655  isismt  27785  nb3grprlem1  28637  vtxdun  28738  rgrx0ndm  28850  ewlksfval  28858  rusgrnumwwlkb0  29225  eclclwwlkn1  29328  avril1  29716  nmoofval  30015  nmooval  30016  nmoo0  30044  nmopval  31109  nmfnval  31129  iunrdx  31795  iinabrex  31800  disjabrex  31813  disjabrexf  31814  dfimafnf  31860  curry2ima  31930  cshwrnid  32125  nsgqusf1olem2  32525  pstmval  32875  pstmfval  32876  sigaval  33109  measval  33196  orvcval  33456  bnj956  33787  bnj18eq1  33938  bnj1318  34036  fnrelpredd  34092  derangval  34158  satfdm  34360  fmlasuc  34377  satffunlem1lem2  34394  satffunlem2lem2  34397  mclsval  34554  dfrdg2  34767  dfrdg3  34768  altxpeq1  34945  altxpeq2  34946  bj-snsetex  35844  bj-sngleq  35848  bj-projeq  35873  bj-projval  35877  bj-imafv  36132  csboprabg  36211  finxpeq1  36267  finxpeq2  36268  csbfinxpg  36269  finxpreclem6  36277  ptrest  36487  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  mblfinlem3  36527  cnambfre  36536  itg2addnc  36542  areacirclem5  36580  sdclem2  36610  sdc  36612  ismtyval  36668  elghomlem1OLD  36753  iineq12f  37032  eccnvepres  37148  lfl1dim  37991  ldual1dim  38036  glbconxN  38249  lineset  38609  pointsetN  38612  psubspset  38615  pmapglb2xN  38643  polval2N  38777  psubclsetN  38807  lautset  38953  pautsetN  38969  tendofset  39629  tendoset  39630  dva1dim  39856  dia1dim2  39933  dib1dim2  40039  diclspsn  40065  dih1dimatlem  40200  dihglb2  40213  hdmap1ffval  40666  hdmapffval  40697  hgmapffval  40756  sticksstones22  40984  prjspeclsp  41354  eldiophb  41495  eldioph  41496  diophrw  41497  eldioph2  41500  eldioph2b  41501  eldioph3  41504  diophin  41510  diophun  41511  diophrex  41513  rexrabdioph  41532  rmxypairf1o  41650  hbtlem1  41865  hbtlem7  41867  tfsconcatrn  42092  nzss  43076  dropab1  43206  dropab2  43207  supsubc  44063  dfaimafn  45873  dfatsnafv2  45960  rnfdmpr  45989  f1oresf1o  45998  imasetpreimafvbijlemfo  46073  fargshiftfo  46110  sprval  46147  sprvalpw  46148  prprval  46182  prprvalpw  46183  prprspr2  46186  pzriprnglem10  46814  pzriprnglem11  46815  setrecseq  47730