Theorem abssdv 3958

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  {cab 2716   ⊆ wss 3843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-v 3400  df-in 3850  df-ss 3860

This theorem is referenced by:  dfopifOLD  4756  opabssxpd  5570  fmpt  6884  eroprf  8426  cfslb2n  9768  rankcf  10277  genpv  10499  genpdm  10502  fimaxre3  11664  supadd  11686  supmul  11690  hashfacenOLD  13905  hashf1lem1OLD  13907  hashf1lem2  13908  mertenslem2  15333  4sqlem11  16391  lss1d  19854  lspsn  19893  lpval  21890  lpsscls  21892  ptuni2  22327  ptbasfi  22332  prdstopn  22379  xkopt  22406  tgpconncompeqg  22863  metrest  23277  mbfeqalem1  24393  limcfval  24624  nmosetre  28699  nmopsetretALT  29798  nmfnsetre  29812  sigaclcuni  31656  bnj849  32476  deranglem  32699  derangsn  32703  nosupno  33547  nosupbday  33549  noinfno  33562  noinfbday  33564  liness  34085  mblfinlem3  35439  ismblfin  35441  itg2addnclem  35451  areacirclem2  35489  sdclem2  35523  sdclem1  35524  ismtyval  35581  heibor1lem  35590  heibor1  35591  pmapglbx  37406  eldiophb  40151  hbtlem2  40521  upbdrech  42382