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  27448  addscom  27452  addsass  27491  mulsval  27568  mulscom  27598  addsdi  27613  mulsass  27624  precsexlemcbv  27655  precsexlem3  27658  isismt  27816  nb3grprlem1  28668  vtxdun  28769  rgrx0ndm  28881  ewlksfval  28889  rusgrnumwwlkb0  29256  eclclwwlkn1  29359  avril1  29747  nmoofval  30046  nmooval  30047  nmoo0  30075  nmopval  31140  nmfnval  31160  iunrdx  31826  iinabrex  31831  disjabrex  31844  disjabrexf  31845  dfimafnf  31891  curry2ima  31961  cshwrnid  32156  nsgqusf1olem2  32556  pstmval  32906  pstmfval  32907  sigaval  33140  measval  33227  orvcval  33487  bnj956  33818  bnj18eq1  33969  bnj1318  34067  fnrelpredd  34123  derangval  34189  satfdm  34391  fmlasuc  34408  satffunlem1lem2  34425  satffunlem2lem2  34428  mclsval  34585  dfrdg2  34798  dfrdg3  34799  altxpeq1  34976  altxpeq2  34977  bj-snsetex  35892  bj-sngleq  35896  bj-projeq  35921  bj-projval  35925  bj-imafv  36180  csboprabg  36259  finxpeq1  36315  finxpeq2  36316  csbfinxpg  36317  finxpreclem6  36325  ptrest  36535  poimirlem26  36562  poimirlem27  36563  poimirlem28  36564  mblfinlem3  36575  cnambfre  36584  itg2addnc  36590  areacirclem5  36628  sdclem2  36658  sdc  36660  ismtyval  36716  elghomlem1OLD  36801  iineq12f  37080  eccnvepres  37196  lfl1dim  38039  ldual1dim  38084  glbconxN  38297  lineset  38657  pointsetN  38660  psubspset  38663  pmapglb2xN  38691  polval2N  38825  psubclsetN  38855  lautset  39001  pautsetN  39017  tendofset  39677  tendoset  39678  dva1dim  39904  dia1dim2  39981  dib1dim2  40087  diclspsn  40113  dih1dimatlem  40248  dihglb2  40261  hdmap1ffval  40714  hdmapffval  40745  hgmapffval  40804  sticksstones22  41032  prjspeclsp  41402  eldiophb  41543  eldioph  41544  diophrw  41545  eldioph2  41548  eldioph2b  41549  eldioph3  41552  diophin  41558  diophun  41559  diophrex  41561  rexrabdioph  41580  rmxypairf1o  41698  hbtlem1  41913  hbtlem7  41915  tfsconcatrn  42140  nzss  43124  dropab1  43254  dropab2  43255  supsubc  44111  dfaimafn  45921  dfatsnafv2  46008  rnfdmpr  46037  f1oresf1o  46046  imasetpreimafvbijlemfo  46121  fargshiftfo  46158  sprval  46195  sprvalpw  46196  prprval  46230  prprvalpw  46231  prprspr2  46234  pzriprnglem10  46862  pzriprnglem11  46863  setrecseq  47778