Theorem abssdv 3995

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.) (Proof shortened by SN, 22-Dec-2024.)

Hypothesis

Ref	Expression
abssdv.1	⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴))

Assertion

Ref	Expression
abssdv	⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem abssdv

Step	Hyp	Ref	Expression
1		abssdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝑥 ∈ 𝐴))
2	1	ss2abdv 3993	. 2 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴})
3		abid1 2900	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
4	2, 3	sseqtrrdi 3954	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  {cab 2741   ⊆ wss 3900

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-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901

This theorem is used by:  dfopif  4842  abexd  5294  opabssxpd  5705  fmpt  7142  fabexd  7983  eroprf  8874  cfslb2n  10385  axdc2lem  10565  rankcf  10901  genpv  11123  genpdm  11126  fimaxre3  12303  supadd  12325  supmul  12329  hashf1lem2  14642  mertenslem2  16098  4sqlem11  17177  lss1d  21289  lspsn  21328  lpval  23512  lpsscls  23514  ptuni2  23950  ptbasfi  23955  prdstopn  24002  xkopt  24029  tgpconncompeqg  24486  metrest  24898  mbfeqalem1  26017  limcfval  26247  nosupno  28117  nosupbday  28119  noinfno  28132  noinfbday  28134  addsproplem2  28413  addsuniflem  28444  addbdaylem  28460  negsid  28484  mulsproplem9  28567  sltmuls1  28590  sltmuls2  28591  precsexlem8  28657  precsexlem11  28660  onaddscl  28720  onmulscl  28721  recut  28937  elreno2  28938  nmosetre  31423  nmopsetretALT  32522  nmfnsetre  32536  sigaclcuni  34861  bnj849  35666  vonf1oonfo  36090  deranglem  36139  derangsn  36143  liness  37125  nmulprop  37154  mblfinlem3  38845  ismblfin  38847  itg2addnclem  38857  areacirclem2  38895  sdclem2  38942  sdclem1  38943  ismtyval  39000  heibor1lem  39009  heibor1  39010  pmapglbx  41092  eldiophb  44034  hbtlem2  44391  oaun3lem1  44637  oaun3lem2  44638  mpoexwd  46187  upbdrech  46594  hoidmvlelem1  47878