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

Theorem trsspwALT3 37271
Description: Short predicate calculus proof of the left-to-right implication of dftr4 4495. 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 37270, which is the virtual deduction proof trsspwALT 37269 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 4499 . . 3  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
2 vex 3034 . . . 4  |-  x  e. 
_V
32elpw 3948 . . 3  |-  ( x  e.  ~P A  <->  x  C_  A
)
41, 3syl6ibr 235 . 2  |-  ( Tr  A  ->  ( x  e.  A  ->  x  e. 
~P A ) )
54ssrdv 3424 1  |-  ( Tr  A  ->  A  C_  ~P A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904    C_ wss 3390   ~Pcpw 3942   Tr wtr 4490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-v 3033  df-in 3397  df-ss 3404  df-pw 3944  df-uni 4191  df-tr 4491
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator