Theorem abssdv 4034

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

Syntax hints:   → wi 4   ∈ wcel 2109  {cab 2708   ⊆ wss 3917

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934

This theorem is referenced by:  dfopif  4837  opabssxpd  5688  fmpt  7085  fabexd  7916  eroprf  8791  cfslb2n  10228  rankcf  10737  genpv  10959  genpdm  10962  fimaxre3  12136  supadd  12158  supmul  12162  hashf1lem2  14428  mertenslem2  15858  4sqlem11  16933  lss1d  20876  lspsn  20915  lpval  23033  lpsscls  23035  ptuni2  23470  ptbasfi  23475  prdstopn  23522  xkopt  23549  tgpconncompeqg  24006  metrest  24419  mbfeqalem1  25549  limcfval  25780  nosupno  27622  nosupbday  27624  noinfno  27637  noinfbday  27639  addsproplem2  27884  addsuniflem  27915  addsbdaylem  27930  negsid  27954  mulsproplem9  28034  ssltmul1  28057  ssltmul2  28058  precsexlem8  28123  precsexlem11  28126  onaddscl  28181  onmulscl  28182  recut  28354  0reno  28355  nmosetre  30700  nmopsetretALT  31799  nmfnsetre  31813  sigaclcuni  34115  bnj849  34922  deranglem  35160  derangsn  35164  liness  36140  mblfinlem3  37660  ismblfin  37662  itg2addnclem  37672  areacirclem2  37710  sdclem2  37743  sdclem1  37744  ismtyval  37801  heibor1lem  37810  heibor1  37811  pmapglbx  39770  eldiophb  42752  hbtlem2  43120  oaun3lem1  43370  oaun3lem2  43371  upbdrech  45310