Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  abssdv GIF version

Theorem abssdv 3139
 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
StepHypRef Expression
1 abssdv.1 . . 3 (𝜑 → (𝜓𝑥𝐴))
21alrimiv 1828 . 2 (𝜑 → ∀𝑥(𝜓𝑥𝐴))
3 abss 3134 . 2 ({𝑥𝜓} ⊆ 𝐴 ↔ ∀𝑥(𝜓𝑥𝐴))
42, 3sylibr 133 1 (𝜑 → {𝑥𝜓} ⊆ 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1312   ∈ wcel 1463  {cab 2101   ⊆ wss 3039 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-in 3045  df-ss 3052 This theorem is referenced by:  fmpt  5536  tfrlemibacc  6189  tfrlemibfn  6191  tfr1onlembacc  6205  tfr1onlembfn  6207  tfrcllembacc  6218  tfrcllembfn  6220  eroprf  6488  genipv  7281  hashfacen  10519  metrest  12570
 Copyright terms: Public domain W3C validator