Theorem abssdv 4062

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

Syntax hints:   → wi 4   ∈ wcel 2099  {cab 2705   ⊆ wss 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962

This theorem is referenced by:  dfopif  4867  opabssxpd  5720  fmpt  7115  eroprf  8828  cfslb2n  10286  rankcf  10795  genpv  11017  genpdm  11020  fimaxre3  12185  supadd  12207  supmul  12211  hashfacenOLD  14441  hashf1lem1OLD  14443  hashf1lem2  14444  mertenslem2  15858  4sqlem11  16918  lss1d  20841  lspsn  20880  lpval  23037  lpsscls  23039  ptuni2  23474  ptbasfi  23479  prdstopn  23526  xkopt  23553  tgpconncompeqg  24010  metrest  24427  mbfeqalem1  25564  limcfval  25795  nosupno  27630  nosupbday  27632  noinfno  27645  noinfbday  27647  addsproplem2  27881  addsuniflem  27912  negsid  27947  mulsproplem9  28018  ssltmul1  28041  ssltmul2  28042  precsexlem8  28106  precsexlem11  28109  recut  28218  0reno  28219  nmosetre  30568  nmopsetretALT  31667  nmfnsetre  31681  sigaclcuni  33732  bnj849  34551  deranglem  34771  derangsn  34775  liness  35736  mblfinlem3  37127  ismblfin  37129  itg2addnclem  37139  areacirclem2  37177  sdclem2  37210  sdclem1  37211  ismtyval  37268  heibor1lem  37277  heibor1  37278  pmapglbx  39237  eldiophb  42168  hbtlem2  42539  oaun3lem1  42794  oaun3lem2  42795  upbdrech  44678