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

Theorem trsspwALT3 31871
Description: Short predicate calculus proof of the left-to-right implication of dftr4 4497. 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 31870, which is the virtual deduction proof trsspwALT 31869 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 4501 . . 3  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
2 vex 3079 . . . 4  |-  x  e. 
_V
32elpw 3973 . . 3  |-  ( x  e.  ~P A  <->  x  C_  A
)
41, 3syl6ibr 227 . 2  |-  ( Tr  A  ->  ( x  e.  A  ->  x  e. 
~P A ) )
54ssrdv 3469 1  |-  ( Tr  A  ->  A  C_  ~P A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758    C_ wss 3435   ~Pcpw 3967   Tr wtr 4492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-v 3078  df-in 3442  df-ss 3449  df-pw 3969  df-uni 4199  df-tr 4493
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator