Theorem abssdv 3639

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

Syntax hints:   → wi 4  ∀wal 1473   ∈ wcel 1977  {cab 2596   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554

This theorem is referenced by:  dfopif  4337  fmpt  6289  opabex2  6997  eroprf  7732  cfslb2n  8973  rankcf  9478  genpv  9700  genpdm  9703  fimaxre3  10849  supadd  10868  supmul  10872  hashfacen  13095  hashf1lem1  13096  hashf1lem2  13097  mertenslem2  14456  4sqlem11  15497  symgbas  17623  lss1d  18784  lspsn  18823  lpval  20753  lpsscls  20755  ptuni2  21189  ptbasfi  21194  prdstopn  21241  xkopt  21268  tgpconcompeqg  21725  metrest  22139  mbfeqalem  23215  limcfval  23442  nmosetre  27003  nmopsetretALT  28106  nmfnsetre  28120  sigaclcuni  29508  bnj849  30249  deranglem  30402  derangsn  30406  liness  31422  mblfinlem3  32618  ismblfin  32620  itg2addnclem  32631  areacirclem2  32671  sdclem2  32708  sdclem1  32709  ismtyval  32769  heibor1lem  32778  heibor1  32779  pmapglbx  34073  eldiophb  36338  hbtlem2  36713  upbdrech  38460