Theorem abbidv 2808

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729

This theorem is referenced by:  rabbidva2  3438  cdeqab  3776  sbceqbid  3795  csbeq1  3902  csbeq2  3904  csbeq2d  3905  csbeq2dv  3906  csbprc  4409  sbcel12  4411  sbceqg  4412  csbnestgfw  4422  csbnestgf  4427  pweqALT  4615  sneq  4636  rabsneq  4644  csbsng  4708  uniprg  4923  csbuni  4936  inteq  4949  iineq1  5009  iineq2  5012  iuneq12d  5021  dfiin2g  5032  iinrab  5069  iinxprg  5089  opabbid  5208  opabbidv  5209  axrep6g  5290  imasng  6102  predres  6360  iotaeq  6526  iotabi  6527  dfimafn  6971  fliftf  7335  oprabbid  7498  oprabbidv  7499  frecseq123  8307  csbfrecsg  8309  wrecseq123OLD  8340  rdglim2  8472  qseq1  8801  qseq2  8802  qsinxp  8833  mapvalg  8876  fsetexb  8904  ixpsnval  8940  ixpeq1  8948  fival  9452  tcvalg  9778  karden  9935  acneq  10083  infmap2  10257  cfval  10287  cflim3  10302  axdclem  10559  axdc  10561  rankcf  10817  genpv  11039  negfi  12217  supadd  12236  hashf1lem2  14495  hashf1  14496  hashfac  14497  csbwrdg  14582  cshimadifsn  14868  cshimadifsn0  14869  cleq1  15022  dfrtrcl2  15101  shftlem  15107  shftfib  15111  vdwlem6  17024  cshwsiun  17137  lubfval  18395  glbfval  18408  eqglact  19197  qus0subgbas  19216  isghm  19233  isghmOLD  19234  symgval  19388  sylow1lem2  19617  sylow3lem1  19645  efgval  19735  dmdprd  20018  ixpsnbasval  21215  pzriprnglem10  21501  pzriprnglem11  21502  cssval  21700  aspval2  21918  ressmplbas2  22045  tgval  22962  clsval2  23058  lpfval  23146  lpval  23147  islocfin  23525  ptval  23578  hauspwpwf1  23995  ptcmplem2  24061  snclseqg  24124  ustval  24211  itg2val  25763  limcfval  25907  plyval  26232  addsval  27995  addscom  27999  addsass  28038  addsbday  28050  mulsval  28135  mulscom  28165  addsdi  28181  mulsass  28192  mulsunif2lem  28195  precsexlemcbv  28230  precsexlem3  28233  halfcut  28416  elreno  28427  readdscl  28431  remulscl  28434  isismt  28542  nb3grprlem1  29397  vtxdun  29499  rgrx0ndm  29611  ewlksfval  29619  rusgrnumwwlkb0  29991  eclclwwlkn1  30094  avril1  30482  nmoofval  30781  nmooval  30782  nmoo0  30810  nmopval  31875  nmfnval  31895  iunrdx  32576  iinabrex  32582  disjabrex  32595  disjabrexf  32596  dfimafnf  32646  curry2ima  32718  cshwrnid  32946  nsgqusf1olem2  33442  pstmval  33894  pstmfval  33895  sigaval  34112  measval  34199  orvcval  34460  bnj956  34790  bnj18eq1  34941  bnj1318  35039  fnrelpredd  35103  derangval  35172  satfdm  35374  fmlasuc  35391  satffunlem1lem2  35408  satffunlem2lem2  35411  mclsval  35568  dfrdg2  35796  dfrdg3  35797  altxpeq1  35974  altxpeq2  35975  ixpeq12dv  36217  cbvcsbdavw  36260  cbvcsbdavw2  36261  cbviundavw  36263  cbviindavw  36264  cbvopab1davw  36265  cbvopab2davw  36266  cbvopabdavw  36267  cbviotadavw  36270  cbvoprab1davw  36272  cbvoprab2davw  36273  cbvoprab3davw  36274  cbvoprab123davw  36275  cbvoprab12davw  36276  cbvoprab23davw  36277  cbvoprab13davw  36278  cbvixpdavw  36279  cbviundavw2  36287  cbviindavw2  36288  cbvixpdavw2  36295  bj-snsetex  36964  bj-sngleq  36968  bj-projeq  36993  bj-projval  36997  bj-imafv  37252  csboprabg  37331  finxpeq1  37387  finxpeq2  37388  csbfinxpg  37389  finxpreclem6  37397  ptrest  37626  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  mblfinlem3  37666  cnambfre  37675  itg2addnc  37681  areacirclem5  37719  sdclem2  37749  sdc  37751  ismtyval  37807  elghomlem1OLD  37892  iineq12f  38171  eccnvepres  38281  lfl1dim  39122  ldual1dim  39167  glbconxN  39380  lineset  39740  pointsetN  39743  psubspset  39746  pmapglb2xN  39774  polval2N  39908  psubclsetN  39938  lautset  40084  pautsetN  40100  tendofset  40760  tendoset  40761  dva1dim  40987  dia1dim2  41064  dib1dim2  41170  diclspsn  41196  dih1dimatlem  41331  dihglb2  41344  hdmap1ffval  41797  hdmapffval  41828  hgmapffval  41887  sticksstones22  42169  sticksstones23  42170  aks6d1c6isolem3  42177  prjspeclsp  42622  sn-isghm  42683  eldiophb  42768  eldioph  42769  diophrw  42770  eldioph2  42773  eldioph2b  42774  eldioph3  42777  diophin  42783  diophun  42784  diophrex  42786  rexrabdioph  42805  rmxypairf1o  42923  hbtlem1  43135  hbtlem7  43137  tfsconcatrn  43355  nzss  44336  dropab1  44466  dropab2  44467  iineq12dv  45111  supsubc  45364  dfaimafn  47177  dfatsnafv2  47264  rnfdmpr  47293  f1oresf1o  47302  imasetpreimafvbijlemfo  47392  fargshiftfo  47429  sprval  47466  sprvalpw  47467  prprval  47501  prprvalpw  47502  prprspr2  47505  isgrim  47868  isgrlim  47949  setrecseq  49204