Theorem abssdv 4029

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

Syntax hints:   → wi 4   ∈ wcel 2149  {cab 2747   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ss 3930

This theorem is referenced by:  dfopif  4839  abexd  5296  opabssxpd  5709  fmpt  7106  fabexd  7934  eroprf  8813  cfslb2n  10252  axdc2lem  10432  rankcf  10762  genpv  10984  genpdm  10987  fimaxre3  12161  supadd  12183  supmul  12187  hashf1lem2  14493  mertenslem2  15939  4sqlem11  17015  lss1d  21062  lspsn  21101  lpval  23265  lpsscls  23267  ptuni2  23702  ptbasfi  23707  prdstopn  23754  xkopt  23781  tgpconncompeqg  24238  metrest  24650  mbfeqalem1  25769  limcfval  26000  nosupno  27833  nosupbday  27835  noinfno  27848  noinfbday  27850  addsproplem2  28129  addsuniflem  28160  addbdaylem  28176  negsid  28200  mulsproplem9  28283  sltmuls1  28306  sltmuls2  28307  precsexlem8  28373  precsexlem11  28376  onaddscl  28436  onmulscl  28437  recut  28653  elreno2  28654  nmosetre  31057  nmopsetretALT  32156  nmfnsetre  32170  sigaclcuni  34453  bnj849  35258  vonf1oonfo  35498  deranglem  35557  derangsn  35561  liness  36536  nmulprop  36581  mblfinlem3  38198  ismblfin  38200  itg2addnclem  38210  areacirclem2  38248  sdclem2  38281  sdclem1  38282  ismtyval  38339  heibor1lem  38348  heibor1  38349  pmapglbx  40433  eldiophb  43380  hbtlem2  43743  oaun3lem1  43993  oaun3lem2  43994  upbdrech  45916  hoidmvlelem1  47201