Theorem abssdv 4078

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

Syntax hints:   → wi 4   ∈ wcel 2106  {cab 2712   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980

This theorem is referenced by:  dfopif  4875  opabssxpd  5736  fmpt  7130  fabexd  7958  eroprf  8854  cfslb2n  10306  rankcf  10815  genpv  11037  genpdm  11040  fimaxre3  12212  supadd  12234  supmul  12238  hashf1lem2  14492  mertenslem2  15918  4sqlem11  16989  lss1d  20979  lspsn  21018  lpval  23163  lpsscls  23165  ptuni2  23600  ptbasfi  23605  prdstopn  23652  xkopt  23679  tgpconncompeqg  24136  metrest  24553  mbfeqalem1  25690  limcfval  25922  nosupno  27763  nosupbday  27765  noinfno  27778  noinfbday  27780  addsproplem2  28018  addsuniflem  28049  addsbdaylem  28064  negsid  28088  mulsproplem9  28165  ssltmul1  28188  ssltmul2  28189  precsexlem8  28253  precsexlem11  28256  onaddscl  28301  onmulscl  28302  recut  28443  0reno  28444  nmosetre  30793  nmopsetretALT  31892  nmfnsetre  31906  sigaclcuni  34099  bnj849  34918  deranglem  35151  derangsn  35155  liness  36127  mblfinlem3  37646  ismblfin  37648  itg2addnclem  37658  areacirclem2  37696  sdclem2  37729  sdclem1  37730  ismtyval  37787  heibor1lem  37796  heibor1  37797  pmapglbx  39752  eldiophb  42745  hbtlem2  43113  oaun3lem1  43364  oaun3lem2  43365  upbdrech  45256