Theorem abbidv 2805

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534   = wceq 1536  {cab 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726

This theorem is referenced by:  rabbidva2  3434  cdeqab  3778  sbceqbid  3797  csbeq1  3910  csbeq2  3912  csbeq2d  3913  csbeq2dv  3914  csbprc  4414  sbcel12  4416  sbceqg  4417  csbnestgfw  4427  csbnestgf  4432  pweqALT  4619  sneq  4640  rabsneq  4648  csbsng  4712  uniprg  4927  csbuni  4940  inteq  4953  iineq1  5013  iineq2  5016  iuneq12d  5025  dfiin2g  5036  iinrab  5073  iinxprg  5093  opabbid  5212  opabbidv  5213  axrep6g  5295  imasng  6103  predres  6361  iotaeq  6527  iotabi  6528  dfimafn  6970  fliftf  7334  oprabbid  7497  oprabbidv  7498  frecseq123  8305  csbfrecsg  8307  wrecseq123OLD  8338  rdglim2  8470  qseq1  8799  qseq2  8800  qsinxp  8831  mapvalg  8874  fsetexb  8902  ixpsnval  8938  ixpeq1  8946  fival  9449  tcvalg  9775  karden  9932  acneq  10080  infmap2  10254  cfval  10284  cflim3  10299  axdclem  10556  axdc  10558  rankcf  10814  genpv  11036  negfi  12214  supadd  12233  hashf1lem2  14491  hashf1  14492  hashfac  14493  csbwrdg  14578  cshimadifsn  14864  cshimadifsn0  14865  cleq1  15018  dfrtrcl2  15097  shftlem  15103  shftfib  15107  vdwlem6  17019  cshwsiun  17133  lubfval  18407  glbfval  18420  eqglact  19209  qus0subgbas  19228  isghm  19245  isghmOLD  19246  symgval  19402  sylow1lem2  19631  sylow3lem1  19659  efgval  19749  dmdprd  20032  ixpsnbasval  21232  pzriprnglem10  21518  pzriprnglem11  21519  cssval  21717  aspval2  21935  ressmplbas2  22062  tgval  22977  clsval2  23073  lpfval  23161  lpval  23162  islocfin  23540  ptval  23593  hauspwpwf1  24010  ptcmplem2  24076  snclseqg  24139  ustval  24226  itg2val  25777  limcfval  25921  plyval  26246  addsval  28009  addscom  28013  addsass  28052  addsbday  28064  mulsval  28149  mulscom  28179  addsdi  28195  mulsass  28206  mulsunif2lem  28209  precsexlemcbv  28244  precsexlem3  28247  halfcut  28430  elreno  28441  readdscl  28445  remulscl  28448  isismt  28556  nb3grprlem1  29411  vtxdun  29513  rgrx0ndm  29625  ewlksfval  29633  rusgrnumwwlkb0  30000  eclclwwlkn1  30103  avril1  30491  nmoofval  30790  nmooval  30791  nmoo0  30819  nmopval  31884  nmfnval  31904  iunrdx  32583  iinabrex  32588  disjabrex  32601  disjabrexf  32602  dfimafnf  32652  curry2ima  32723  cshwrnid  32930  nsgqusf1olem2  33421  pstmval  33855  pstmfval  33856  sigaval  34091  measval  34178  orvcval  34438  bnj956  34768  bnj18eq1  34919  bnj1318  35017  fnrelpredd  35081  derangval  35151  satfdm  35353  fmlasuc  35370  satffunlem1lem2  35387  satffunlem2lem2  35390  mclsval  35547  dfrdg2  35776  dfrdg3  35777  altxpeq1  35954  altxpeq2  35955  ixpeq12dv  36198  cbvcsbdavw  36241  cbvcsbdavw2  36242  cbviundavw  36244  cbviindavw  36245  cbvopab1davw  36246  cbvopab2davw  36247  cbvopabdavw  36248  cbviotadavw  36251  cbvoprab1davw  36253  cbvoprab2davw  36254  cbvoprab3davw  36255  cbvoprab123davw  36256  cbvoprab12davw  36257  cbvoprab23davw  36258  cbvoprab13davw  36259  cbvixpdavw  36260  cbviundavw2  36268  cbviindavw2  36269  cbvixpdavw2  36276  bj-snsetex  36945  bj-sngleq  36949  bj-projeq  36974  bj-projval  36978  bj-imafv  37233  csboprabg  37312  finxpeq1  37368  finxpeq2  37369  csbfinxpg  37370  finxpreclem6  37378  ptrest  37605  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  mblfinlem3  37645  cnambfre  37654  itg2addnc  37660  areacirclem5  37698  sdclem2  37728  sdc  37730  ismtyval  37786  elghomlem1OLD  37871  iineq12f  38150  eccnvepres  38261  lfl1dim  39102  ldual1dim  39147  glbconxN  39360  lineset  39720  pointsetN  39723  psubspset  39726  pmapglb2xN  39754  polval2N  39888  psubclsetN  39918  lautset  40064  pautsetN  40080  tendofset  40740  tendoset  40741  dva1dim  40967  dia1dim2  41044  dib1dim2  41150  diclspsn  41176  dih1dimatlem  41311  dihglb2  41324  hdmap1ffval  41777  hdmapffval  41808  hgmapffval  41867  sticksstones22  42149  sticksstones23  42150  aks6d1c6isolem3  42157  prjspeclsp  42598  sn-isghm  42659  eldiophb  42744  eldioph  42745  diophrw  42746  eldioph2  42749  eldioph2b  42750  eldioph3  42753  diophin  42759  diophun  42760  diophrex  42762  rexrabdioph  42781  rmxypairf1o  42899  hbtlem1  43111  hbtlem7  43113  tfsconcatrn  43331  nzss  44312  dropab1  44442  dropab2  44443  iineq12dv  45045  supsubc  45302  dfaimafn  47114  dfatsnafv2  47201  rnfdmpr  47230  f1oresf1o  47239  imasetpreimafvbijlemfo  47329  fargshiftfo  47366  sprval  47403  sprvalpw  47404  prprval  47438  prprvalpw  47439  prprspr2  47442  isgrim  47805  isgrlim  47884  setrecseq  48915