Theorem abssdv 4007

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2714   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3906

This theorem is referenced by:  dfopif  4813  abexd  5266  opabssxpd  5678  fmpt  7062  fabexd  7888  eroprf  8762  cfslb2n  10190  axdc2lem  10370  rankcf  10700  genpv  10922  genpdm  10925  fimaxre3  12102  supadd  12124  supmul  12128  hashf1lem2  14418  mertenslem2  15850  4sqlem11  16926  lss1d  20958  lspsn  20997  lpval  23104  lpsscls  23106  ptuni2  23541  ptbasfi  23546  prdstopn  23593  xkopt  23620  tgpconncompeqg  24077  metrest  24489  mbfeqalem1  25608  limcfval  25839  nosupno  27667  nosupbday  27669  noinfno  27682  noinfbday  27684  addsproplem2  27962  addsuniflem  27993  addbdaylem  28009  negsid  28033  mulsproplem9  28116  sltmuls1  28139  sltmuls2  28140  precsexlem8  28206  precsexlem11  28209  onaddscl  28269  onmulscl  28270  recut  28486  elreno2  28487  nmosetre  30835  nmopsetretALT  31934  nmfnsetre  31948  sigaclcuni  34262  bnj849  35067  deranglem  35348  derangsn  35352  liness  36327  mblfinlem3  37980  ismblfin  37982  itg2addnclem  37992  areacirclem2  38030  sdclem2  38063  sdclem1  38064  ismtyval  38121  heibor1lem  38130  heibor1  38131  pmapglbx  40215  eldiophb  43189  hbtlem2  43552  oaun3lem1  43802  oaun3lem2  43803  upbdrech  45738  hoidmvlelem1  47023