Description: Short predicate calculus proof of the left-to-right implication of dftr4 . 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 , which is the virtual deduction proof trsspwALT without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | trsspwALT3 | |- ( Tr A -> A C_ ~P A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trss | |- ( Tr A -> ( x e. A -> x C_ A ) ) |
|
| 2 | vex | |- x e. _V |
|
| 3 | 2 | elpw | |- ( x e. ~P A <-> x C_ A ) |
| 4 | 1 3 | imbitrrdi | |- ( Tr A -> ( x e. A -> x e. ~P A ) ) |
| 5 | 4 | ssrdv | |- ( Tr A -> A C_ ~P A ) |