Theorem abssdv 4030

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

Syntax hints:   → wi 4   ∈ wcel 2106  {cab 2708   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  dfopif  4832  opabssxpd  5684  fmpt  7063  eroprf  8761  cfslb2n  10213  rankcf  10722  genpv  10944  genpdm  10947  fimaxre3  12110  supadd  12132  supmul  12136  hashfacenOLD  14364  hashf1lem1OLD  14366  hashf1lem2  14367  mertenslem2  15781  4sqlem11  16838  lss1d  20481  lspsn  20520  lpval  22527  lpsscls  22529  ptuni2  22964  ptbasfi  22969  prdstopn  23016  xkopt  23043  tgpconncompeqg  23500  metrest  23917  mbfeqalem1  25042  limcfval  25273  nosupno  27088  nosupbday  27090  noinfno  27103  noinfbday  27105  addsproplem2  27325  addsunif  27353  negsid  27382  mulsproplem10  27431  nmosetre  29769  nmopsetretALT  30868  nmfnsetre  30882  sigaclcuni  32806  bnj849  33626  deranglem  33847  derangsn  33851  liness  34806  mblfinlem3  36190  ismblfin  36192  itg2addnclem  36202  areacirclem2  36240  sdclem2  36274  sdclem1  36275  ismtyval  36332  heibor1lem  36341  heibor1  36342  pmapglbx  38305  eldiophb  41138  hbtlem2  41509  oaun3lem1  41767  oaun3lem2  41768  upbdrech  43660