Theorem abbidv 2802

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2184, 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 1928	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		abbi 2801	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
4	2, 3	syl 17	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728

This theorem is referenced by:  rabbidva2  3401  cdeqab  3728  sbceqbid  3747  csbeq1  3852  csbeq2  3854  csbeq2d  3855  csbeq2dv  3856  csbprc  4361  sbcel12  4363  sbceqg  4364  csbnestgfw  4374  csbnestgf  4379  pweqALT  4569  sneq  4590  rabsneq  4599  csbsng  4665  uniprg  4879  csbuni  4893  inteq  4905  iineq1  4964  iineq2  4967  iuneq12d  4976  dfiin2g  4986  iinrab  5024  iinxprg  5044  opabbid  5163  opabbidv  5164  axrep6g  5235  imasng  6043  predres  6297  iotaeq  6460  iotabi  6461  dfimafn  6896  fliftf  7261  oprabbid  7423  oprabbidv  7424  frecseq123  8224  csbfrecsg  8226  rdglim2  8363  qseq1  8694  qseq2  8695  qsinxp  8730  mapvalg  8773  fsetexb  8801  ixpsnval  8838  ixpeq1  8846  fival  9315  tcvalg  9645  karden  9807  acneq  9953  infmap2  10127  cfval  10157  cflim3  10172  axdclem  10429  axdc  10431  rankcf  10688  genpv  10910  negfi  12091  supadd  12110  hashf1lem2  14379  hashf1  14380  hashfac  14381  csbwrdg  14467  cshimadifsn  14752  cshimadifsn0  14753  cleq1  14906  dfrtrcl2  14985  shftlem  14991  shftfib  14995  vdwlem6  16914  cshwsiun  17027  lubfval  18271  glbfval  18284  eqglact  19108  qus0subgbas  19127  isghm  19144  isghmOLD  19145  symgval  19300  sylow1lem2  19528  sylow3lem1  19556  efgval  19646  dmdprd  19929  ixpsnbasval  21160  pzriprnglem10  21445  pzriprnglem11  21446  cssval  21637  aspval2  21854  ressmplbas2  21982  tgval  22899  clsval2  22994  lpfval  23082  lpval  23083  islocfin  23461  ptval  23514  hauspwpwf1  23931  ptcmplem2  23997  snclseqg  24060  ustval  24147  itg2val  25685  limcfval  25829  plyval  26154  addsval  27958  addscom  27962  addsass  28001  addbday  28014  mulsval  28105  mulscom  28135  addsdi  28151  mulsass  28162  mulsunif2lem  28165  precsexlemcbv  28202  precsexlem3  28205  halfcut  28454  pw2cut2  28458  elreno  28487  readdscl  28495  remulscl  28498  isismt  28606  nb3grprlem1  29453  vtxdun  29555  rgrx0ndm  29667  ewlksfval  29675  rusgrnumwwlkb0  30047  eclclwwlkn1  30150  avril1  30538  nmoofval  30837  nmooval  30838  nmoo0  30866  nmopval  31931  nmfnval  31951  iunrdx  32638  iinabrex  32644  disjabrex  32657  disjabrexf  32658  dfimafnf  32714  curry2ima  32788  cshwrnid  33043  nsgqusf1olem2  33495  pstmval  34052  pstmfval  34053  sigaval  34268  measval  34355  orvcval  34615  bnj956  34932  bnj18eq1  35083  bnj1318  35181  fnrelpredd  35247  derangval  35361  satfdm  35563  fmlasuc  35580  satffunlem1lem2  35597  satffunlem2lem2  35600  mclsval  35757  dfrdg2  35987  dfrdg3  35988  altxpeq1  36167  altxpeq2  36168  ixpeq12dv  36410  cbvcsbdavw  36453  cbvcsbdavw2  36454  cbviundavw  36456  cbviindavw  36457  cbvopab1davw  36458  cbvopab2davw  36459  cbvopabdavw  36460  cbviotadavw  36463  cbvoprab1davw  36465  cbvoprab2davw  36466  cbvoprab3davw  36467  cbvoprab123davw  36468  cbvoprab12davw  36469  cbvoprab23davw  36470  cbvoprab13davw  36471  cbvixpdavw  36472  cbviundavw2  36480  cbviindavw2  36481  cbvixpdavw2  36488  bj-snsetex  37164  bj-sngleq  37168  bj-projeq  37193  bj-projval  37197  bj-imafv  37452  csboprabg  37531  finxpeq1  37587  finxpeq2  37588  csbfinxpg  37589  finxpreclem6  37597  ptrest  37816  poimirlem26  37843  poimirlem27  37844  poimirlem28  37845  mblfinlem3  37856  cnambfre  37865  itg2addnc  37871  areacirclem5  37909  sdclem2  37939  sdc  37941  ismtyval  37997  elghomlem1OLD  38082  iineq12f  38361  eccnvepres  38475  lfl1dim  39377  ldual1dim  39422  glbconxN  39634  lineset  39994  pointsetN  39997  psubspset  40000  pmapglb2xN  40028  polval2N  40162  psubclsetN  40192  lautset  40338  pautsetN  40354  tendofset  41014  tendoset  41015  dva1dim  41241  dia1dim2  41318  dib1dim2  41424  diclspsn  41450  dih1dimatlem  41585  dihglb2  41598  hdmap1ffval  42051  hdmapffval  42082  hgmapffval  42141  sticksstones22  42418  sticksstones23  42419  aks6d1c6isolem3  42426  prjspeclsp  42851  sn-isghm  42912  eldiophb  42995  eldioph  42996  diophrw  42997  eldioph2  43000  eldioph2b  43001  eldioph3  43004  diophin  43010  diophun  43011  diophrex  43013  rexrabdioph  43032  rmxypairf1o  43149  hbtlem1  43361  hbtlem7  43363  tfsconcatrn  43580  nzss  44554  dropab1  44683  dropab2  44684  iineq12dv  45346  supsubc  45594  dfaimafn  47407  dfatsnafv2  47494  rnfdmpr  47523  f1oresf1o  47532  imasetpreimafvbijlemfo  47647  fargshiftfo  47684  sprval  47721  sprvalpw  47722  prprval  47756  prprvalpw  47757  prprspr2  47760  isgrim  48124  isgrlim  48224  setrecseq  49926