Theorem abssdv 4008

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

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

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 3907

This theorem is referenced by:  dfopif  4814  abexd  5263  opabssxpd  5672  fmpt  7057  fabexd  7882  eroprf  8756  cfslb2n  10184  axdc2lem  10364  rankcf  10694  genpv  10916  genpdm  10919  fimaxre3  12096  supadd  12118  supmul  12122  hashf1lem2  14412  mertenslem2  15844  4sqlem11  16920  lss1d  20952  lspsn  20991  lpval  23117  lpsscls  23119  ptuni2  23554  ptbasfi  23559  prdstopn  23606  xkopt  23633  tgpconncompeqg  24090  metrest  24502  mbfeqalem1  25621  limcfval  25852  nosupno  27684  nosupbday  27686  noinfno  27699  noinfbday  27701  addsproplem2  27979  addsuniflem  28010  addbdaylem  28026  negsid  28050  mulsproplem9  28133  sltmuls1  28156  sltmuls2  28157  precsexlem8  28223  precsexlem11  28226  onaddscl  28286  onmulscl  28287  recut  28503  elreno2  28504  nmosetre  30853  nmopsetretALT  31952  nmfnsetre  31966  sigaclcuni  34281  bnj849  35086  deranglem  35367  derangsn  35371  liness  36346  mblfinlem3  37997  ismblfin  37999  itg2addnclem  38009  areacirclem2  38047  sdclem2  38080  sdclem1  38081  ismtyval  38138  heibor1lem  38147  heibor1  38148  pmapglbx  40232  eldiophb  43206  hbtlem2  43573  oaun3lem1  43823  oaun3lem2  43824  upbdrech  45759  hoidmvlelem1  47044