Theorem abssdv 4031

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 4029	. 2 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ {𝑥 ∣ 𝑥 ∈ 𝐴})
3		abid1 2864	. 2 ⊢ 𝐴 = {𝑥 ∣ 𝑥 ∈ 𝐴}
4	2, 3	sseqtrrdi 3988	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2707   ⊆ wss 3914

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-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931

This theorem is referenced by:  dfopif  4834  opabssxpd  5685  fmpt  7082  fabexd  7913  eroprf  8788  cfslb2n  10221  rankcf  10730  genpv  10952  genpdm  10955  fimaxre3  12129  supadd  12151  supmul  12155  hashf1lem2  14421  mertenslem2  15851  4sqlem11  16926  lss1d  20869  lspsn  20908  lpval  23026  lpsscls  23028  ptuni2  23463  ptbasfi  23468  prdstopn  23515  xkopt  23542  tgpconncompeqg  23999  metrest  24412  mbfeqalem1  25542  limcfval  25773  nosupno  27615  nosupbday  27617  noinfno  27630  noinfbday  27632  addsproplem2  27877  addsuniflem  27908  addsbdaylem  27923  negsid  27947  mulsproplem9  28027  ssltmul1  28050  ssltmul2  28051  precsexlem8  28116  precsexlem11  28119  onaddscl  28174  onmulscl  28175  recut  28347  0reno  28348  nmosetre  30693  nmopsetretALT  31792  nmfnsetre  31806  sigaclcuni  34108  bnj849  34915  deranglem  35153  derangsn  35157  liness  36133  mblfinlem3  37653  ismblfin  37655  itg2addnclem  37665  areacirclem2  37703  sdclem2  37736  sdclem1  37737  ismtyval  37794  heibor1lem  37803  heibor1  37804  pmapglbx  39763  eldiophb  42745  hbtlem2  43113  oaun3lem1  43363  oaun3lem2  43364  upbdrech  45303