Theorem abssdv 4028

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

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

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 3928

This theorem is referenced by:  dfopif  4830  opabssxpd  5678  fmpt  7064  fabexd  7893  eroprf  8765  cfslb2n  10197  rankcf  10706  genpv  10928  genpdm  10931  fimaxre3  12105  supadd  12127  supmul  12131  hashf1lem2  14397  mertenslem2  15827  4sqlem11  16902  lss1d  20845  lspsn  20884  lpval  23002  lpsscls  23004  ptuni2  23439  ptbasfi  23444  prdstopn  23491  xkopt  23518  tgpconncompeqg  23975  metrest  24388  mbfeqalem1  25518  limcfval  25749  nosupno  27591  nosupbday  27593  noinfno  27606  noinfbday  27608  addsproplem2  27853  addsuniflem  27884  addsbdaylem  27899  negsid  27923  mulsproplem9  28003  ssltmul1  28026  ssltmul2  28027  precsexlem8  28092  precsexlem11  28095  onaddscl  28150  onmulscl  28151  recut  28323  0reno  28324  nmosetre  30666  nmopsetretALT  31765  nmfnsetre  31779  sigaclcuni  34081  bnj849  34888  deranglem  35126  derangsn  35130  liness  36106  mblfinlem3  37626  ismblfin  37628  itg2addnclem  37638  areacirclem2  37676  sdclem2  37709  sdclem1  37710  ismtyval  37767  heibor1lem  37776  heibor1  37777  pmapglbx  39736  eldiophb  42718  hbtlem2  43086  oaun3lem1  43336  oaun3lem2  43337  upbdrech  45276