Theorem abssdv 4065

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

Syntax hints:   → wi 4   ∈ wcel 2106  {cab 2709   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  dfopif  4870  opabssxpd  5723  fmpt  7111  eroprf  8811  cfslb2n  10265  rankcf  10774  genpv  10996  genpdm  10999  fimaxre3  12164  supadd  12186  supmul  12190  hashfacenOLD  14418  hashf1lem1OLD  14420  hashf1lem2  14421  mertenslem2  15835  4sqlem11  16892  lss1d  20718  lspsn  20757  lpval  22863  lpsscls  22865  ptuni2  23300  ptbasfi  23305  prdstopn  23352  xkopt  23379  tgpconncompeqg  23836  metrest  24253  mbfeqalem1  25382  limcfval  25613  nosupno  27430  nosupbday  27432  noinfno  27445  noinfbday  27447  addsproplem2  27680  addsuniflem  27711  negsid  27742  mulsproplem9  27807  ssltmul1  27829  ssltmul2  27830  precsexlem8  27887  precsexlem11  27890  nmosetre  30272  nmopsetretALT  31371  nmfnsetre  31385  sigaclcuni  33402  bnj849  34222  deranglem  34443  derangsn  34447  liness  35409  mblfinlem3  36830  ismblfin  36832  itg2addnclem  36842  areacirclem2  36880  sdclem2  36913  sdclem1  36914  ismtyval  36971  heibor1lem  36980  heibor1  36981  pmapglbx  38943  eldiophb  41797  hbtlem2  42168  oaun3lem1  42426  oaun3lem2  42427  upbdrech  44314