Theorem abbidv 2802

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2178, 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 2801	. 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 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  rabbidva2  3422  cdeqab  3758  sbceqbid  3777  csbeq1  3882  csbeq2  3884  csbeq2d  3885  csbeq2dv  3886  csbprc  4389  sbcel12  4391  sbceqg  4392  csbnestgfw  4402  csbnestgf  4407  pweqALT  4595  sneq  4616  rabsneq  4625  csbsng  4689  uniprg  4904  csbuni  4917  inteq  4930  iineq1  4990  iineq2  4993  iuneq12d  5002  dfiin2g  5013  iinrab  5050  iinxprg  5070  opabbid  5189  opabbidv  5190  axrep6g  5265  imasng  6076  predres  6333  iotaeq  6501  iotabi  6502  dfimafn  6946  fliftf  7313  oprabbid  7477  oprabbidv  7478  frecseq123  8286  csbfrecsg  8288  wrecseq123OLD  8319  rdglim2  8451  qseq1  8780  qseq2  8781  qsinxp  8812  mapvalg  8855  fsetexb  8883  ixpsnval  8919  ixpeq1  8927  fival  9429  tcvalg  9757  karden  9914  acneq  10062  infmap2  10236  cfval  10266  cflim3  10281  axdclem  10538  axdc  10540  rankcf  10796  genpv  11018  negfi  12196  supadd  12215  hashf1lem2  14479  hashf1  14480  hashfac  14481  csbwrdg  14567  cshimadifsn  14853  cshimadifsn0  14854  cleq1  15007  dfrtrcl2  15086  shftlem  15092  shftfib  15096  vdwlem6  17011  cshwsiun  17124  lubfval  18365  glbfval  18378  eqglact  19167  qus0subgbas  19186  isghm  19203  isghmOLD  19204  symgval  19357  sylow1lem2  19585  sylow3lem1  19613  efgval  19703  dmdprd  19986  ixpsnbasval  21171  pzriprnglem10  21456  pzriprnglem11  21457  cssval  21647  aspval2  21863  ressmplbas2  21990  tgval  22898  clsval2  22993  lpfval  23081  lpval  23082  islocfin  23460  ptval  23513  hauspwpwf1  23930  ptcmplem2  23996  snclseqg  24059  ustval  24146  itg2val  25686  limcfval  25830  plyval  26155  addsval  27926  addscom  27930  addsass  27969  addsbday  27981  mulsval  28069  mulscom  28099  addsdi  28115  mulsass  28126  mulsunif2lem  28129  precsexlemcbv  28165  precsexlem3  28168  halfcut  28390  elreno  28403  readdscl  28407  remulscl  28410  isismt  28518  nb3grprlem1  29364  vtxdun  29466  rgrx0ndm  29578  ewlksfval  29586  rusgrnumwwlkb0  29958  eclclwwlkn1  30061  avril1  30449  nmoofval  30748  nmooval  30749  nmoo0  30777  nmopval  31842  nmfnval  31862  iunrdx  32549  iinabrex  32555  disjabrex  32568  disjabrexf  32569  dfimafnf  32619  curry2ima  32691  cshwrnid  32942  nsgqusf1olem2  33434  pstmval  33931  pstmfval  33932  sigaval  34147  measval  34234  orvcval  34495  bnj956  34812  bnj18eq1  34963  bnj1318  35061  fnrelpredd  35125  derangval  35194  satfdm  35396  fmlasuc  35413  satffunlem1lem2  35430  satffunlem2lem2  35433  mclsval  35590  dfrdg2  35818  dfrdg3  35819  altxpeq1  35996  altxpeq2  35997  ixpeq12dv  36239  cbvcsbdavw  36282  cbvcsbdavw2  36283  cbviundavw  36285  cbviindavw  36286  cbvopab1davw  36287  cbvopab2davw  36288  cbvopabdavw  36289  cbviotadavw  36292  cbvoprab1davw  36294  cbvoprab2davw  36295  cbvoprab3davw  36296  cbvoprab123davw  36297  cbvoprab12davw  36298  cbvoprab23davw  36299  cbvoprab13davw  36300  cbvixpdavw  36301  cbviundavw2  36309  cbviindavw2  36310  cbvixpdavw2  36317  bj-snsetex  36986  bj-sngleq  36990  bj-projeq  37015  bj-projval  37019  bj-imafv  37274  csboprabg  37353  finxpeq1  37409  finxpeq2  37410  csbfinxpg  37411  finxpreclem6  37419  ptrest  37648  poimirlem26  37675  poimirlem27  37676  poimirlem28  37677  mblfinlem3  37688  cnambfre  37697  itg2addnc  37703  areacirclem5  37741  sdclem2  37771  sdc  37773  ismtyval  37829  elghomlem1OLD  37914  iineq12f  38193  eccnvepres  38303  lfl1dim  39144  ldual1dim  39189  glbconxN  39402  lineset  39762  pointsetN  39765  psubspset  39768  pmapglb2xN  39796  polval2N  39930  psubclsetN  39960  lautset  40106  pautsetN  40122  tendofset  40782  tendoset  40783  dva1dim  41009  dia1dim2  41086  dib1dim2  41192  diclspsn  41218  dih1dimatlem  41353  dihglb2  41366  hdmap1ffval  41819  hdmapffval  41850  hgmapffval  41909  sticksstones22  42186  sticksstones23  42187  aks6d1c6isolem3  42194  prjspeclsp  42610  sn-isghm  42671  eldiophb  42755  eldioph  42756  diophrw  42757  eldioph2  42760  eldioph2b  42761  eldioph3  42764  diophin  42770  diophun  42771  diophrex  42773  rexrabdioph  42792  rmxypairf1o  42910  hbtlem1  43122  hbtlem7  43124  tfsconcatrn  43341  nzss  44316  dropab1  44446  dropab2  44447  iineq12dv  45110  supsubc  45360  dfaimafn  47174  dfatsnafv2  47261  rnfdmpr  47290  f1oresf1o  47299  imasetpreimafvbijlemfo  47399  fargshiftfo  47436  sprval  47473  sprvalpw  47474  prprval  47508  prprvalpw  47509  prprspr2  47512  isgrim  47875  isgrlim  47974  setrecseq  49529