Theorem abssdv 3998

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  dfopifOLD  4798  opabssxpd  5625  fmpt  6966  eroprf  8562  cfslb2n  9955  rankcf  10464  genpv  10686  genpdm  10689  fimaxre3  11851  supadd  11873  supmul  11877  hashfacenOLD  14095  hashf1lem1OLD  14097  hashf1lem2  14098  mertenslem2  15525  4sqlem11  16584  lss1d  20140  lspsn  20179  lpval  22198  lpsscls  22200  ptuni2  22635  ptbasfi  22640  prdstopn  22687  xkopt  22714  tgpconncompeqg  23171  metrest  23586  mbfeqalem1  24710  limcfval  24941  nmosetre  29027  nmopsetretALT  30126  nmfnsetre  30140  sigaclcuni  31986  bnj849  32805  deranglem  33028  derangsn  33032  nosupno  33833  nosupbday  33835  noinfno  33848  noinfbday  33850  liness  34374  mblfinlem3  35743  ismblfin  35745  itg2addnclem  35755  areacirclem2  35793  sdclem2  35827  sdclem1  35828  ismtyval  35885  heibor1lem  35894  heibor1  35895  pmapglbx  37710  eldiophb  40495  hbtlem2  40865  upbdrech  42734