Theorem abssdv 4021

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

Syntax hints:   → wi 4   ∈ wcel 2114  {cab 2715   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3920

This theorem is referenced by:  dfopif  4828  abexd  5272  opabssxpd  5679  fmpt  7064  fabexd  7889  eroprf  8764  cfslb2n  10190  axdc2lem  10370  rankcf  10700  genpv  10922  genpdm  10925  fimaxre3  12100  supadd  12122  supmul  12126  hashf1lem2  14391  mertenslem2  15820  4sqlem11  16895  lss1d  20926  lspsn  20965  lpval  23095  lpsscls  23097  ptuni2  23532  ptbasfi  23537  prdstopn  23584  xkopt  23611  tgpconncompeqg  24068  metrest  24480  mbfeqalem1  25610  limcfval  25841  nosupno  27683  nosupbday  27685  noinfno  27698  noinfbday  27700  addsproplem2  27978  addsuniflem  28009  addbdaylem  28025  negsid  28049  mulsproplem9  28132  sltmuls1  28155  sltmuls2  28156  precsexlem8  28222  precsexlem11  28225  onaddscl  28285  onmulscl  28286  recut  28502  elreno2  28503  nmosetre  30852  nmopsetretALT  31951  nmfnsetre  31965  sigaclcuni  34296  bnj849  35101  deranglem  35382  derangsn  35386  liness  36361  mblfinlem3  37910  ismblfin  37912  itg2addnclem  37922  areacirclem2  37960  sdclem2  37993  sdclem1  37994  ismtyval  38051  heibor1lem  38060  heibor1  38061  pmapglbx  40145  eldiophb  43114  hbtlem2  43481  oaun3lem1  43731  oaun3lem2  43732  upbdrech  45667  hoidmvlelem1  46953