Theorem abssdv 4044

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

Syntax hints:   → wi 4  ∀wal 1531   ∈ wcel 2110  {cab 2799   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-in 3942  df-ss 3951

This theorem is referenced by:  dfopif  4793  opabssxpd  5783  fmpt  6868  eroprf  8389  cfslb2n  9684  rankcf  10193  genpv  10415  genpdm  10418  fimaxre3  11581  supadd  11603  supmul  11607  hashfacen  13806  hashf1lem1  13807  hashf1lem2  13808  mertenslem2  15235  4sqlem11  16285  lss1d  19729  lspsn  19768  lpval  21741  lpsscls  21743  ptuni2  22178  ptbasfi  22183  prdstopn  22230  xkopt  22257  tgpconncompeqg  22714  metrest  23128  mbfeqalem1  24236  limcfval  24464  nmosetre  28535  nmopsetretALT  29634  nmfnsetre  29648  sigaclcuni  31372  bnj849  32192  deranglem  32408  derangsn  32412  nosupno  33198  nosupbday  33200  liness  33601  mblfinlem3  34925  ismblfin  34927  itg2addnclem  34937  areacirclem2  34977  sdclem2  35011  sdclem1  35012  ismtyval  35072  heibor1lem  35081  heibor1  35082  pmapglbx  36899  eldiophb  39347  hbtlem2  39717  upbdrech  41565