Theorem abssdv 4068

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cab 2714   ⊆ wss 3951

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968

This theorem is referenced by:  dfopif  4870  opabssxpd  5732  fmpt  7130  fabexd  7959  eroprf  8855  cfslb2n  10308  rankcf  10817  genpv  11039  genpdm  11042  fimaxre3  12214  supadd  12236  supmul  12240  hashf1lem2  14495  mertenslem2  15921  4sqlem11  16993  lss1d  20961  lspsn  21000  lpval  23147  lpsscls  23149  ptuni2  23584  ptbasfi  23589  prdstopn  23636  xkopt  23663  tgpconncompeqg  24120  metrest  24537  mbfeqalem1  25676  limcfval  25907  nosupno  27748  nosupbday  27750  noinfno  27763  noinfbday  27765  addsproplem2  28003  addsuniflem  28034  addsbdaylem  28049  negsid  28073  mulsproplem9  28150  ssltmul1  28173  ssltmul2  28174  precsexlem8  28238  precsexlem11  28241  onaddscl  28286  onmulscl  28287  recut  28428  0reno  28429  nmosetre  30783  nmopsetretALT  31882  nmfnsetre  31896  sigaclcuni  34119  bnj849  34939  deranglem  35171  derangsn  35175  liness  36146  mblfinlem3  37666  ismblfin  37668  itg2addnclem  37678  areacirclem2  37716  sdclem2  37749  sdclem1  37750  ismtyval  37807  heibor1lem  37816  heibor1  37817  pmapglbx  39771  eldiophb  42768  hbtlem2  43136  oaun3lem1  43387  oaun3lem2  43388  upbdrech  45317