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

Syntax hints:   → wi 4   ∈ wcel 2142  {cab 2740   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3921

This theorem is referenced by:  dfopif  4828  abexd  5281  opabssxpd  5694  fmpt  7091  fabexd  7918  eroprf  8797  cfslb2n  10225  axdc2lem  10405  rankcf  10735  genpv  10957  genpdm  10960  fimaxre3  12138  supadd  12160  supmul  12164  hashf1lem2  14469  mertenslem2  15915  4sqlem11  16991  lss1d  21030  lspsn  21069  lpval  23199  lpsscls  23201  ptuni2  23636  ptbasfi  23641  prdstopn  23688  xkopt  23715  tgpconncompeqg  24172  metrest  24584  mbfeqalem1  25703  limcfval  25934  nosupno  27767  nosupbday  27769  noinfno  27782  noinfbday  27784  addsproplem2  28063  addsuniflem  28094  addbdaylem  28110  negsid  28134  mulsproplem9  28217  sltmuls1  28240  sltmuls2  28241  precsexlem8  28307  precsexlem11  28310  onaddscl  28370  onmulscl  28371  recut  28587  elreno2  28588  nmosetre  30967  nmopsetretALT  32066  nmfnsetre  32080  sigaclcuni  34415  bnj849  35220  vonf1oonfo  35458  deranglem  35516  derangsn  35520  liness  36495  nmulprop  36540  mblfinlem3  38158  ismblfin  38160  itg2addnclem  38170  areacirclem2  38208  sdclem2  38241  sdclem1  38242  ismtyval  38299  heibor1lem  38308  heibor1  38309  pmapglbx  40393  eldiophb  43338  hbtlem2  43701  oaun3lem1  43951  oaun3lem2  43952  upbdrech  45884  hoidmvlelem1  47169