Theorem abssdv 3998

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

Syntax hints:   → wi 4   ∈ wcel 2119  {cab 2717   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ss 3900

This theorem is referenced by:  dfopif  4801  abexd  5253  opabssxpd  5665  fmpt  7051  fabexd  7877  eroprf  8752  cfslb2n  10181  axdc2lem  10361  rankcf  10691  genpv  10913  genpdm  10916  fimaxre3  12093  supadd  12115  supmul  12119  hashf1lem2  14409  mertenslem2  15841  4sqlem11  16917  lss1d  20953  lspsn  20992  lpval  23122  lpsscls  23124  ptuni2  23559  ptbasfi  23564  prdstopn  23611  xkopt  23638  tgpconncompeqg  24095  metrest  24507  mbfeqalem1  25626  limcfval  25857  nosupno  27685  nosupbday  27687  noinfno  27700  noinfbday  27702  addsproplem2  27980  addsuniflem  28011  addbdaylem  28027  negsid  28051  mulsproplem9  28134  sltmuls1  28157  sltmuls2  28158  precsexlem8  28224  precsexlem11  28227  onaddscl  28287  onmulscl  28288  recut  28504  elreno2  28505  nmosetre  30853  nmopsetretALT  31952  nmfnsetre  31966  sigaclcuni  34302  bnj849  35107  deranglem  35394  derangsn  35398  liness  36373  mblfinlem3  38026  ismblfin  38028  itg2addnclem  38038  areacirclem2  38076  sdclem2  38109  sdclem1  38110  ismtyval  38167  heibor1lem  38176  heibor1  38177  pmapglbx  40261  eldiophb  43206  hbtlem2  43569  oaun3lem1  43819  oaun3lem2  43820  upbdrech  45753  hoidmvlelem1  47038