MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss2abdv Structured version   Visualization version   GIF version

Theorem ss2abdv 3708
Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.)
Hypothesis
Ref Expression
ss2abdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ss2abdv (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem ss2abdv
StepHypRef Expression
1 ss2abdv.1 . . 3 (𝜑 → (𝜓𝜒))
21alrimiv 1895 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 ss2ab 3703 . 2 ({𝑥𝜓} ⊆ {𝑥𝜒} ↔ ∀𝑥(𝜓𝜒))
42, 3sylibr 224 1 (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  {cab 2637  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621
This theorem is referenced by:  intss  4530  ssopab2  5030  ssoprab2  6753  suppimacnvss  7350  suppimacnv  7351  ressuppss  7359  ss2ixp  7963  fiss  8371  tcss  8658  tcel  8659  infmap2  9078  cfub  9109  cflm  9110  cflecard  9113  clsslem  13769  cncmet  23165  plyss  24000  ofrn2  29570  sigaclci  30323  subfacp1lem6  31293  ss2mcls  31591  itg2addnclem  33591  sdclem1  33669  istotbnd3  33700  sstotbnd  33704  qsss1  34194  aomclem4  37944  hbtlem4  38013  hbtlem3  38014  rngunsnply  38060  iocinico  38114
  Copyright terms: Public domain W3C validator