Theorem abssdv 4017

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

Syntax hints:   → wi 4   ∈ wcel 2113  {cab 2712   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ss 3916

This theorem is referenced by:  dfopif  4824  abexd  5268  opabssxpd  5669  fmpt  7053  fabexd  7877  eroprf  8750  cfslb2n  10176  axdc2lem  10356  rankcf  10686  genpv  10908  genpdm  10911  fimaxre3  12086  supadd  12108  supmul  12112  hashf1lem2  14377  mertenslem2  15806  4sqlem11  16881  lss1d  20912  lspsn  20951  lpval  23081  lpsscls  23083  ptuni2  23518  ptbasfi  23523  prdstopn  23570  xkopt  23597  tgpconncompeqg  24054  metrest  24466  mbfeqalem1  25596  limcfval  25827  nosupno  27669  nosupbday  27671  noinfno  27684  noinfbday  27686  addsproplem2  27940  addsuniflem  27971  addsbdaylem  27986  negsid  28010  mulsproplem9  28093  ssltmul1  28116  ssltmul2  28117  precsexlem8  28182  precsexlem11  28185  onaddscl  28241  onmulscl  28242  recut  28439  elreno2  28440  nmosetre  30788  nmopsetretALT  31887  nmfnsetre  31901  sigaclcuni  34224  bnj849  35030  deranglem  35309  derangsn  35313  liness  36288  mblfinlem3  37799  ismblfin  37801  itg2addnclem  37811  areacirclem2  37849  sdclem2  37882  sdclem1  37883  ismtyval  37940  heibor1lem  37949  heibor1  37950  pmapglbx  39968  eldiophb  42941  hbtlem2  43308  oaun3lem1  43558  oaun3lem2  43559  upbdrech  45495  hoidmvlelem1  46781