Theorem abssdv 4022

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  {cab 2743   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3923

This theorem is used by:  dfopif  4837  abexd  5298  opabssxpd  5710  fmpt  7109  fabexd  7940  eroprf  8819  cfslb2n  10267  axdc2lem  10447  rankcf  10779  genpv  11001  genpdm  11004  fimaxre3  12178  supadd  12200  supmul  12204  hashf1lem2  14513  mertenslem2  15964  4sqlem11  17039  lss1d  21136  lspsn  21175  lpval  23348  lpsscls  23350  ptuni2  23786  ptbasfi  23791  prdstopn  23838  xkopt  23865  tgpconncompeqg  24322  metrest  24734  mbfeqalem1  25853  limcfval  26084  nosupno  27920  nosupbday  27922  noinfno  27935  noinfbday  27937  addsproplem2  28216  addsuniflem  28247  addbdaylem  28263  negsid  28287  mulsproplem9  28370  sltmuls1  28393  sltmuls2  28394  precsexlem8  28460  precsexlem11  28463  onaddscl  28523  onmulscl  28524  recut  28740  elreno2  28741  nmosetre  31189  nmopsetretALT  32288  nmfnsetre  32302  sigaclcuni  34574  bnj849  35380  vonf1oonfo  35658  deranglem  35697  derangsn  35701  liness  36676  nmulprop  36721  mblfinlem3  38369  ismblfin  38371  itg2addnclem  38381  areacirclem2  38419  sdclem2  38453  sdclem1  38454  ismtyval  38511  heibor1lem  38520  heibor1  38521  pmapglbx  40603  eldiophb  43548  hbtlem2  43911  oaun3lem1  44161  oaun3lem2  44162  upbdrech  46084  hoidmvlelem1  47369