Theorem abssdv 4002

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2106  {cab 2715   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  dfopifOLD  4801  opabssxpd  5634  fmpt  6984  eroprf  8604  cfslb2n  10024  rankcf  10533  genpv  10755  genpdm  10758  fimaxre3  11921  supadd  11943  supmul  11947  hashfacenOLD  14167  hashf1lem1OLD  14169  hashf1lem2  14170  mertenslem2  15597  4sqlem11  16656  lss1d  20225  lspsn  20264  lpval  22290  lpsscls  22292  ptuni2  22727  ptbasfi  22732  prdstopn  22779  xkopt  22806  tgpconncompeqg  23263  metrest  23680  mbfeqalem1  24805  limcfval  25036  nmosetre  29126  nmopsetretALT  30225  nmfnsetre  30239  sigaclcuni  32086  bnj849  32905  deranglem  33128  derangsn  33132  nosupno  33906  nosupbday  33908  noinfno  33921  noinfbday  33923  liness  34447  mblfinlem3  35816  ismblfin  35818  itg2addnclem  35828  areacirclem2  35866  sdclem2  35900  sdclem1  35901  ismtyval  35958  heibor1lem  35967  heibor1  35968  pmapglbx  37783  eldiophb  40579  hbtlem2  40949  upbdrech  42844