Theorem abssdv 4020

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

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

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 3920

This theorem is referenced by:  dfopif  4821  opabssxpd  5666  fmpt  7044  fabexd  7870  eroprf  8742  cfslb2n  10162  rankcf  10671  genpv  10893  genpdm  10896  fimaxre3  12071  supadd  12093  supmul  12097  hashf1lem2  14363  mertenslem2  15792  4sqlem11  16867  lss1d  20866  lspsn  20905  lpval  23024  lpsscls  23026  ptuni2  23461  ptbasfi  23466  prdstopn  23513  xkopt  23540  tgpconncompeqg  23997  metrest  24410  mbfeqalem1  25540  limcfval  25771  nosupno  27613  nosupbday  27615  noinfno  27628  noinfbday  27630  addsproplem2  27882  addsuniflem  27913  addsbdaylem  27928  negsid  27952  mulsproplem9  28032  ssltmul1  28055  ssltmul2  28056  precsexlem8  28121  precsexlem11  28124  onaddscl  28179  onmulscl  28180  recut  28365  0reno  28366  nmosetre  30708  nmopsetretALT  31807  nmfnsetre  31821  sigaclcuni  34085  bnj849  34892  deranglem  35143  derangsn  35147  liness  36123  mblfinlem3  37643  ismblfin  37645  itg2addnclem  37655  areacirclem2  37693  sdclem2  37726  sdclem1  37727  ismtyval  37784  heibor1lem  37793  heibor1  37794  pmapglbx  39752  eldiophb  42734  hbtlem2  43101  oaun3lem1  43351  oaun3lem2  43352  upbdrech  45291