Theorem abssdv 4091

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cab 2717   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993

This theorem is referenced by:  dfopif  4894  opabssxpd  5747  fmpt  7144  fabexd  7975  eroprf  8873  cfslb2n  10337  rankcf  10846  genpv  11068  genpdm  11071  fimaxre3  12241  supadd  12263  supmul  12267  hashf1lem2  14505  mertenslem2  15933  4sqlem11  17002  lss1d  20984  lspsn  21023  lpval  23168  lpsscls  23170  ptuni2  23605  ptbasfi  23610  prdstopn  23657  xkopt  23684  tgpconncompeqg  24141  metrest  24558  mbfeqalem1  25695  limcfval  25927  nosupno  27766  nosupbday  27768  noinfno  27781  noinfbday  27783  addsproplem2  28021  addsuniflem  28052  addsbdaylem  28067  negsid  28091  mulsproplem9  28168  ssltmul1  28191  ssltmul2  28192  precsexlem8  28256  precsexlem11  28259  onaddscl  28304  onmulscl  28305  recut  28446  0reno  28447  nmosetre  30796  nmopsetretALT  31895  nmfnsetre  31909  sigaclcuni  34082  bnj849  34901  deranglem  35134  derangsn  35138  liness  36109  mblfinlem3  37619  ismblfin  37621  itg2addnclem  37631  areacirclem2  37669  sdclem2  37702  sdclem1  37703  ismtyval  37760  heibor1lem  37769  heibor1  37770  pmapglbx  39726  eldiophb  42713  hbtlem2  43081  oaun3lem1  43336  oaun3lem2  43337  upbdrech  45220