Theorem abssdv 4043

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

Syntax hints:   → wi 4   ∈ wcel 2108  {cab 2713   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943

This theorem is referenced by:  dfopif  4846  opabssxpd  5701  fmpt  7100  fabexd  7933  eroprf  8829  cfslb2n  10282  rankcf  10791  genpv  11013  genpdm  11016  fimaxre3  12188  supadd  12210  supmul  12214  hashf1lem2  14474  mertenslem2  15901  4sqlem11  16975  lss1d  20920  lspsn  20959  lpval  23077  lpsscls  23079  ptuni2  23514  ptbasfi  23519  prdstopn  23566  xkopt  23593  tgpconncompeqg  24050  metrest  24463  mbfeqalem1  25594  limcfval  25825  nosupno  27667  nosupbday  27669  noinfno  27682  noinfbday  27684  addsproplem2  27929  addsuniflem  27960  addsbdaylem  27975  negsid  27999  mulsproplem9  28079  ssltmul1  28102  ssltmul2  28103  precsexlem8  28168  precsexlem11  28171  onaddscl  28226  onmulscl  28227  recut  28399  0reno  28400  nmosetre  30745  nmopsetretALT  31844  nmfnsetre  31858  sigaclcuni  34149  bnj849  34956  deranglem  35188  derangsn  35192  liness  36163  mblfinlem3  37683  ismblfin  37685  itg2addnclem  37695  areacirclem2  37733  sdclem2  37766  sdclem1  37767  ismtyval  37824  heibor1lem  37833  heibor1  37834  pmapglbx  39788  eldiophb  42780  hbtlem2  43148  oaun3lem1  43398  oaun3lem2  43399  upbdrech  45334