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

Theorem trsspwALT3 34012
Description: Short predicate calculus proof of the left-to-right implication of dftr4 4537. 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 34011, which is the virtual deduction proof trsspwALT 34010 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 4541 . . 3  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
2 vex 3109 . . . 4  |-  x  e. 
_V
32elpw 4005 . . 3  |-  ( x  e.  ~P A  <->  x  C_  A
)
41, 3syl6ibr 227 . 2  |-  ( Tr  A  ->  ( x  e.  A  ->  x  e. 
~P A ) )
54ssrdv 3495 1  |-  ( Tr  A  ->  A  C_  ~P A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823    C_ wss 3461   ~Pcpw 3999   Tr wtr 4532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108  df-in 3468  df-ss 3475  df-pw 4001  df-uni 4236  df-tr 4533
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator