Theorem abbidv 2797

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  rabbidva2  3397  cdeqab  3729  sbceqbid  3748  csbeq1  3853  csbeq2  3855  csbeq2d  3856  csbeq2dv  3857  csbprc  4359  sbcel12  4361  sbceqg  4362  csbnestgfw  4372  csbnestgf  4377  pweqALT  4565  sneq  4586  rabsneq  4595  csbsng  4661  uniprg  4875  csbuni  4888  inteq  4900  iineq1  4959  iineq2  4962  iuneq12d  4971  dfiin2g  4981  iinrab  5017  iinxprg  5037  opabbid  5156  opabbidv  5157  axrep6g  5228  imasng  6033  predres  6286  iotaeq  6449  iotabi  6450  dfimafn  6884  fliftf  7249  oprabbid  7411  oprabbidv  7412  frecseq123  8212  csbfrecsg  8214  rdglim2  8351  qseq1  8681  qseq2  8682  qsinxp  8717  mapvalg  8760  fsetexb  8788  ixpsnval  8824  ixpeq1  8832  fival  9296  tcvalg  9628  karden  9785  acneq  9931  infmap2  10105  cfval  10135  cflim3  10150  axdclem  10407  axdc  10409  rankcf  10665  genpv  10887  negfi  12068  supadd  12087  hashf1lem2  14360  hashf1  14361  hashfac  14362  csbwrdg  14448  cshimadifsn  14733  cshimadifsn0  14734  cleq1  14887  dfrtrcl2  14966  shftlem  14972  shftfib  14976  vdwlem6  16895  cshwsiun  17008  lubfval  18251  glbfval  18264  eqglact  19089  qus0subgbas  19108  isghm  19125  isghmOLD  19126  symgval  19281  sylow1lem2  19509  sylow3lem1  19537  efgval  19627  dmdprd  19910  ixpsnbasval  21140  pzriprnglem10  21425  pzriprnglem11  21426  cssval  21617  aspval2  21833  ressmplbas2  21960  tgval  22868  clsval2  22963  lpfval  23051  lpval  23052  islocfin  23430  ptval  23483  hauspwpwf1  23900  ptcmplem2  23966  snclseqg  24029  ustval  24116  itg2val  25654  limcfval  25798  plyval  26123  addsval  27903  addscom  27907  addsass  27946  addsbday  27958  mulsval  28046  mulscom  28076  addsdi  28092  mulsass  28103  mulsunif2lem  28106  precsexlemcbv  28142  precsexlem3  28145  halfcut  28376  pw2cut2  28380  elreno  28395  readdscl  28399  remulscl  28402  isismt  28510  nb3grprlem1  29356  vtxdun  29458  rgrx0ndm  29570  ewlksfval  29578  rusgrnumwwlkb0  29947  eclclwwlkn1  30050  avril1  30438  nmoofval  30737  nmooval  30738  nmoo0  30766  nmopval  31831  nmfnval  31851  iunrdx  32538  iinabrex  32544  disjabrex  32557  disjabrexf  32558  dfimafnf  32613  curry2ima  32685  cshwrnid  32937  nsgqusf1olem2  33374  pstmval  33903  pstmfval  33904  sigaval  34119  measval  34206  orvcval  34466  bnj956  34783  bnj18eq1  34934  bnj1318  35032  fnrelpredd  35097  derangval  35199  satfdm  35401  fmlasuc  35418  satffunlem1lem2  35435  satffunlem2lem2  35438  mclsval  35595  dfrdg2  35828  dfrdg3  35829  altxpeq1  36006  altxpeq2  36007  ixpeq12dv  36249  cbvcsbdavw  36292  cbvcsbdavw2  36293  cbviundavw  36295  cbviindavw  36296  cbvopab1davw  36297  cbvopab2davw  36298  cbvopabdavw  36299  cbviotadavw  36302  cbvoprab1davw  36304  cbvoprab2davw  36305  cbvoprab3davw  36306  cbvoprab123davw  36307  cbvoprab12davw  36308  cbvoprab23davw  36309  cbvoprab13davw  36310  cbvixpdavw  36311  cbviundavw2  36319  cbviindavw2  36320  cbvixpdavw2  36327  bj-snsetex  36996  bj-sngleq  37000  bj-projeq  37025  bj-projval  37029  bj-imafv  37284  csboprabg  37363  finxpeq1  37419  finxpeq2  37420  csbfinxpg  37421  finxpreclem6  37429  ptrest  37658  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  mblfinlem3  37698  cnambfre  37707  itg2addnc  37713  areacirclem5  37751  sdclem2  37781  sdc  37783  ismtyval  37839  elghomlem1OLD  37924  iineq12f  38203  eccnvepres  38313  lfl1dim  39159  ldual1dim  39204  glbconxN  39416  lineset  39776  pointsetN  39779  psubspset  39782  pmapglb2xN  39810  polval2N  39944  psubclsetN  39974  lautset  40120  pautsetN  40136  tendofset  40796  tendoset  40797  dva1dim  41023  dia1dim2  41100  dib1dim2  41206  diclspsn  41232  dih1dimatlem  41367  dihglb2  41380  hdmap1ffval  41833  hdmapffval  41864  hgmapffval  41923  sticksstones22  42200  sticksstones23  42201  aks6d1c6isolem3  42208  prjspeclsp  42644  sn-isghm  42705  eldiophb  42789  eldioph  42790  diophrw  42791  eldioph2  42794  eldioph2b  42795  eldioph3  42798  diophin  42804  diophun  42805  diophrex  42807  rexrabdioph  42826  rmxypairf1o  42943  hbtlem1  43155  hbtlem7  43157  tfsconcatrn  43374  nzss  44349  dropab1  44478  dropab2  44479  iineq12dv  45142  supsubc  45391  dfaimafn  47195  dfatsnafv2  47282  rnfdmpr  47311  f1oresf1o  47320  imasetpreimafvbijlemfo  47435  fargshiftfo  47472  sprval  47509  sprvalpw  47510  prprval  47544  prprvalpw  47545  prprspr2  47548  isgrim  47912  isgrlim  48012  setrecseq  49716