Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pwtrrOLD Unicode version

Theorem pwtrrOLD 27974
 Description: A set is transitive if its power set is. The proof of this theorem was automatically generated from pwtrrVD 27973 using a tools command file, translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Moved into main set.mm as pwtr 4226 and may be deleted by mathbox owner, AS. --NM 15-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
pwtrr.1
Assertion
Ref Expression
pwtrrOLD

Proof of Theorem pwtrrOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 19 . . . . . 6
2 simpr 447 . . . . . . 7
32a1i 10 . . . . . 6
4 pwtrr.1 . . . . . . 7
54pwid 3638 . . . . . 6
6 trel 4120 . . . . . . 7
76exp3a 425 . . . . . 6
81, 3, 5, 7ee120 27809 . . . . 5
9 elpwi 3633 . . . . 5
108, 9syl6 29 . . . 4
11 simpl 443 . . . . 5
1211a1i 10 . . . 4
13 ssel 3174 . . . 4
1410, 12, 13ee22 1352 . . 3
1514alrimivv 1618 . 2
16 dftr2 4115 . 2
1715, 16sylibr 203 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358  wal 1527   wcel 1684  cvv 2788   wss 3152  cpw 3625   wtr 4113 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627  df-uni 3828  df-tr 4114
 Copyright terms: Public domain W3C validator