Theorem abbidv 2827

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   = wceq 1559  {cab 2739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753

This theorem is referenced by:  rabbidva2  3415  cdeqab  3732  sbceqbid  3751  csbeq1  3855  csbeq2  3857  csbeq2d  3858  csbeq2dv  3859  csbprc  4362  sbcel12  4364  sbceqg  4365  csbnestgfw  4375  csbnestgf  4380  pweqALT  4569  sneq  4591  csbsng  4666  uniprg  4880  csbuni  4895  inteq  4907  iineq1  4966  iineq2  4969  iuneq12d  4978  dfiin2g  4987  iinrab  5025  iinxprg  5045  opabbid  5164  opabbidv  5165  axrep6g  5239  imasng  6070  predres  6322  iotaeq  6485  iotabi  6486  dfimafn  6925  fliftf  7295  oprabbid  7457  oprabbidv  7458  frecseq123  8258  csbfrecsg  8260  rdglim2  8398  qseq1  8733  qseq2  8734  snecg  8754  qsinxp  8770  mapvalg  8813  fsetexb  8841  ixpsnval  8878  ixpeq1  8886  fival  9355  tcvalg  9688  karden  9850  acneq  9996  infmap2  10170  cfval  10200  cflim3  10216  axdclem  10473  axdc  10475  rankcf  10732  genpv  10954  negfi  12138  supadd  12157  hashf1lem2  14466  hashf1  14467  hashfac  14468  csbwrdg  14554  cshimadifsn  14839  cshimadifsn0  14840  cleq1  14993  dfrtrcl2  15072  shftlem  15078  shftfib  15082  vdwlem6  17005  cshwsiun  17118  lubfval  18363  glbfval  18376  eqglact  19203  qus0subgbas  19222  isghm  19239  symgval  19394  sylow1lem2  19622  sylow3lem1  19650  efgval  19740  dmdprd  20023  ixpsnbasval  21255  pzriprnglem10  21522  pzriprnglem11  21523  cssval  21714  aspval2  21930  ressmplbas2  22059  tgval  22995  clsval2  23090  lpfval  23178  lpval  23179  islocfin  23557  ptval  23610  hauspwpwf1  24027  ptcmplem2  24093  snclseqg  24156  ustval  24243  itg2val  25770  limcfval  25914  plyval  26233  addsval  28032  addscom  28036  addsass  28075  addbday  28088  mulsval  28179  mulscom  28209  addsdi  28225  mulsass  28236  mulsunif2lem  28239  precsexlemcbv  28276  precsexlem3  28279  halfcut  28528  pw2cut2  28532  elreno  28561  readdscl  28569  remulscl  28572  isismt  28680  nb3grprlem1  29527  vtxdun  29628  rgrx0ndm  29740  ewlksfval  29748  rusgrnumwwlkb0  30120  eclclwwlkn1  30223  avril1  30611  nmoofval  30911  nmooval  30912  nmoo0  30940  nmopval  32005  nmfnval  32025  iunrdx  32712  iinabrex  32718  disjabrex  32731  disjabrexf  32732  dfimafnf  32788  curry2ima  32861  cshwrnid  33100  nsgqusf1olem2  33561  pstmval  34153  pstmfval  34154  sigaval  34369  measval  34456  orvcval  34716  bnj956  35036  bnj18eq1  35186  bnj1318  35284  fnrelpredd  35351  derangval  35481  satfdm  35683  fmlasuc  35700  satffunlem1lem2  35717  satffunlem2lem2  35720  mclsval  35877  dfrdg2  36107  dfrdg3  36108  altxpeq1  36287  altxpeq2  36288  ixpeq12dv  36540  cbvcsbdavw  36583  cbvcsbdavw2  36584  cbviundavw  36586  cbviindavw  36587  cbvopab1davw  36588  cbvopab2davw  36589  cbvopabdavw  36590  cbviotadavw  36593  cbvoprab1davw  36595  cbvoprab2davw  36596  cbvoprab3davw  36597  cbvoprab123davw  36598  cbvoprab12davw  36599  cbvoprab23davw  36600  cbvoprab13davw  36601  cbvixpdavw  36602  cbviundavw2  36610  cbviindavw2  36611  cbvixpdavw2  36618  bj-snsetex  37412  bj-sngleq  37416  bj-projeq  37441  bj-projval  37445  bj-imafv  37707  csboprabg  37788  finxpeq1  37844  finxpeq2  37845  csbfinxpg  37846  finxpreclem6  37854  ptrest  38082  poimirlem26  38109  poimirlem27  38110  poimirlem28  38111  mblfinlem3  38122  cnambfre  38131  itg2addnc  38137  areacirclem5  38175  sdclem2  38205  sdc  38207  ismtyval  38263  elghomlem1OLD  38348  iineq12f  38627  eccnvepres  38749  ecqmap  38912  lfl1dim  39709  ldual1dim  39754  glbconxN  39966  lineset  40326  pointsetN  40329  psubspset  40332  pmapglb2xN  40360  polval2N  40494  psubclsetN  40524  lautset  40670  pautsetN  40686  tendofset  41346  tendoset  41347  dva1dim  41573  dia1dim2  41650  dib1dim2  41756  diclspsn  41782  dih1dimatlem  41917  dihglb2  41930  hdmap1ffval  42383  hdmapffval  42414  hgmapffval  42473  sticksstones22  42749  sticksstones23  42750  aks6d1c6isolem3  42757  prjspeclsp  43158  sn-isghm  43219  eldiophb  43302  eldioph  43303  diophrw  43304  eldioph2  43307  eldioph2b  43308  eldioph3  43311  diophin  43317  diophun  43318  diophrex  43320  rexrabdioph  43335  rmxypairf1o  43452  hbtlem1  43664  hbtlem7  43666  tfsconcatrn  43883  nzss  44857  dropab1  44986  dropab2  44987  iineq12dv  45648  supsubc  45893  dfaimafn  47723  dfatsnafv2  47810  rnfdmpr  47839  f1oresf1o  47848  imasetpreimafvbijlemfo  47975  fargshiftfo  48012  sprval  48049  sprvalpw  48050  prprval  48084  prprvalpw  48085  prprspr2  48088  isgrim  48468  isgrlim  48568  setrecseq  50270