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

Theorem ss2abdv 4041
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 1919 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 ss2ab 4036 . 2 ({𝑥𝜓} ⊆ {𝑥𝜒} ↔ ∀𝑥(𝜓𝜒))
42, 3sylibr 235 1 (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526  {cab 2796  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-in 3940  df-ss 3949
This theorem is referenced by:  intss  4888  ssopab2  5424  ssoprab2  7211  suppimacnvss  7829  suppimacnv  7830  ressuppss  7838  ss2ixp  8462  fiss  8876  tcss  9174  tcel  9175  infmap2  9628  cfub  9659  cflm  9660  cflecard  9663  clsslem  14332  cncmet  23852  plyss  24716  iunrnmptss  30245  ofrn2  30315  sigaclci  31290  subfacp1lem6  32329  ss2mcls  32712  itg2addnclem  34824  sdclem1  34899  istotbnd3  34930  sstotbnd  34934  qsss1  35426  aomclem4  39535  hbtlem4  39604  hbtlem3  39605  rngunsnply  39651  iocinico  39696
  Copyright terms: Public domain W3C validator