Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trsspwALT3 Structured version   Unicode version

Theorem trsspwALT3 31483
Description: Short predicate calculus proof of the left-to-right implication of dftr4 4385. A transitive class is a subset of its power class. This proof was constructed by applying Metamath's minimize command to the proof of trsspwALT2 31482, which is the virtual deduction proof trsspwALT 31481 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
trsspwALT3  |-  ( Tr  A  ->  A  C_  ~P A )

Proof of Theorem trsspwALT3
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 trss 4389 . . 3  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
2 vex 2970 . . . 4  |-  x  e. 
_V
32elpw 3861 . . 3  |-  ( x  e.  ~P A  <->  x  C_  A
)
41, 3syl6ibr 227 . 2  |-  ( Tr  A  ->  ( x  e.  A  ->  x  e. 
~P A ) )
54ssrdv 3357 1  |-  ( Tr  A  ->  A  C_  ~P A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3323   ~Pcpw 3855   Tr wtr 4380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-v 2969  df-in 3330  df-ss 3337  df-pw 3857  df-uni 4087  df-tr 4381
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator