Theorem abssdv 3996

Description: Deduction of abstraction subclass from implication. (Contributed by NM, 20-Jan-2006.)

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	alrimiv 1928	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 → 𝑥 ∈ 𝐴))
3		abss 3988	. 2 ⊢ ({𝑥 ∣ 𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓 → 𝑥 ∈ 𝐴))
4	2, 3	sylibr 237	1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1536   ∈ wcel 2111  {cab 2776   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  dfopif  4760  opabssxpd  5753  fmpt  6851  eroprf  8378  cfslb2n  9679  rankcf  10188  genpv  10410  genpdm  10413  fimaxre3  11575  supadd  11596  supmul  11600  hashfacen  13808  hashf1lem1  13809  hashf1lem2  13810  mertenslem2  15233  4sqlem11  16281  lss1d  19728  lspsn  19767  lpval  21744  lpsscls  21746  ptuni2  22181  ptbasfi  22186  prdstopn  22233  xkopt  22260  tgpconncompeqg  22717  metrest  23131  mbfeqalem1  24245  limcfval  24475  nmosetre  28547  nmopsetretALT  29646  nmfnsetre  29660  sigaclcuni  31487  bnj849  32307  deranglem  32526  derangsn  32530  nosupno  33316  nosupbday  33318  liness  33719  mblfinlem3  35096  ismblfin  35098  itg2addnclem  35108  areacirclem2  35146  sdclem2  35180  sdclem1  35181  ismtyval  35238  heibor1lem  35247  heibor1  35248  pmapglbx  37065  eldiophb  39698  hbtlem2  40068  upbdrech  41937