Theorem abbidv 2829

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755

This theorem is used by:  rabbidva2  3418  cdeqab  3731  sbceqbid  3749  csbeq1  3854  csbeq2  3856  csbeq2d  3857  csbeq2dv  3858  csbprc  4370  sbcel12  4372  sbceqg  4373  csbnestgfw  4383  csbnestgf  4388  pweqALT  4575  sneq  4594  csbsng  4669  uniprg  4886  csbuni  4901  inteq  4913  iineq1  4972  iineq2  4975  iuneq12d  4983  dfiin2g  4992  iinrab  5030  iinxprg  5052  opabbid  5174  opabbidv  5175  axrep6g  5247  dfrn7  6079  imasng  6095  predres  6363  iotaeq  6527  iotabi  6528  dfimafn  6973  fliftf  7349  oprabbid  7511  oprabbidv  7512  frecseq123  8331  csbfrecsg  8333  rdglim2  8471  qseq1  8808  qseq2  8809  snecg  8829  qsinxp  8845  mapvalg  8887  fsetexb  8917  ixpsnval  8959  ixpeq1  8967  fival  9434  tcvalg  9767  karden  9989  kardenOLD  9990  acneq  10152  infmap2  10325  cfval  10354  cflim3  10370  axdclem  10627  axdc  10629  rankcf  10892  genpv  11114  negfi  12296  supadd  12315  hashf1lem2  14631  hashf1  14632  hashfac  14633  csbwrdg  14719  cshimadifsn  15011  cshimadifsn0  15012  cleq1  15168  dfrtrcl2  15247  shftlem  15253  shftfib  15257  vdwlem6  17196  cshwsiun  17309  lubfval  18554  glbfval  18567  eqglact  19423  qus0subgbas  19445  isghm  19462  symgval  19618  sylow1lem2  19846  sylow3lem1  19874  efgval  19964  dmdprd  20247  ixpsnbasval  21516  pzriprnglem10  21829  pzriprnglem11  21830  cssval  22021  aspval2  22239  ressmplbas2  22368  tgval  23306  clsval2  23401  lpfval  23489  lpval  23490  islocfin  23869  ptval  23922  hauspwpwf1  24339  ptcmplem2  24405  snclseqg  24468  ustval  24555  itg2val  26082  limcfval  26225  plyval  26544  addsval  28381  addscom  28385  addsass  28424  addbday  28437  mulsval  28528  mulscom  28558  addsdi  28574  mulsass  28585  mulsunif2lem  28588  precsexlemcbv  28625  precsexlem3  28628  halfcut  28877  pw2cut2  28881  elreno  28910  readdscl  28918  remulscl  28921  isismt  29030  nb3grprlem1  29994  vtxdun  30095  rgrx0ndm  30207  ewlksfval  30215  rusgrnumwwlkb0  30596  eclclwwlkn1  30699  avril1  31097  nmoofval  31397  nmooval  31398  nmoo0  31426  nmopval  32491  nmfnval  32511  iunrdx  33233  iinabrex  33238  disjabrex  33251  disjabrexf  33252  dfimafnf  33305  curry2ima  33376  cshwrnid  33595  nsgqusf1olem2  34049  pstmval  34610  pstmfval  34611  sigaval  34826  measval  34914  orvcval  35173  bnj956  35490  bnj18eq1  35640  bnj1318  35738  fnrelpredd  35817  erscottd  35856  ecscottd  35857  kardval  35933  kard0  35935  derangval  36112  satfdm  36314  fmlasuc  36331  satffunlem1lem2  36348  satffunlem2lem2  36351  mclsval  36508  dfrdg2  36748  dfrdg3  36749  altxpeq1  36929  altxpeq2  36930  ixpeq12dv  37196  cbvcsbdavw  37239  cbvcsbdavw2  37240  cbviundavw  37242  cbviindavw  37243  cbvopab1davw  37244  cbvopab2davw  37245  cbvopabdavw  37246  cbviotadavw  37249  cbvoprab1davw  37251  cbvoprab2davw  37252  cbvoprab3davw  37253  cbvoprab123davw  37254  cbvoprab12davw  37255  cbvoprab23davw  37256  cbvoprab13davw  37257  cbvixpdavw  37258  cbviundavw2  37266  cbviindavw2  37267  cbvixpdavw2  37274  bj-snsetex  38067  bj-sngleq  38071  bj-projeq  38096  bj-projval  38100  bj-imafv  38377  csboprabg  38458  finxpeq1  38514  finxpeq2  38515  csbfinxpg  38516  finxpreclem6  38524  ptrest  38742  poimirlem26  38769  poimirlem27  38770  poimirlem28  38771  mblfinlem3  38782  cnambfre  38791  itg2addnc  38797  areacirclem5  38835  varprop  38847  negprop  38848  impprop  38849  dfprop2  38851  sdclem2  38879  sdc  38881  ismtyval  38937  elghomlem1OLD  39022  iineq12f  39299  eccnvepres  39421  ecqmap  39584  lfl1dim  40381  ldual1dim  40426  glbconxN  40638  lineset  40998  pointsetN  41001  psubspset  41004  pmapglb2xN  41032  polval2N  41166  psubclsetN  41196  lautset  41342  pautsetN  41358  tendofset  42018  tendoset  42019  dva1dim  42245  dia1dim2  42322  dib1dim2  42428  diclspsn  42454  dih1dimatlem  42589  dihglb2  42602  hdmap1ffval  43055  hdmapffval  43086  hgmapffval  43145  sticksstones22  43421  sticksstones23  43422  aks6d1c6isolem3  43429  prjspeclsp  43844  sn-isghm  43888  eldiophb  43972  eldioph  43973  diophrw  43974  eldioph2  43977  eldioph2b  43978  eldioph3  43981  diophin  43987  diophun  43988  diophrex  43990  rexrabdioph  44005  rmxypairf1o  44122  hbtlem1  44328  hbtlem7  44330  tfsconcatrn  44547  nzss  45504  dropab1  45632  dropab2  45633  iineq12dv  46336  supsubc  46580  dfaimafn  48450  dfatsnafv2  48537  rnfdmpr  48566  f1oresf1o  48575  imasetpreimafvbijlemfo  48702  fargshiftfo  48739  sprval  48776  sprvalpw  48777  prprval  48811  prprvalpw  48812  prprspr2  48815  isgrim  49195  isgrlim  49295  setrecseq  51078