Theorem trsspwALT

Description: Virtual deduction proof of the left-to-right implication of dftr4 . A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	trsspwALT	|- ( Tr A -> A C_ ~P A )

Proof

Step	Hyp	Ref	Expression
1		df-ss	|- ( A C_ ~P A <-> A. x ( x e. A -> x e. ~P A ) )
2		idn1	|- (. Tr A ->. Tr A ).
3		idn2	|- (. Tr A ,. x e. A ->. x e. A ).
4		trss	|- ( Tr A -> ( x e. A -> x C_ A ) )
5	2 3 4	e12	|- (. Tr A ,. x e. A ->. x C_ A ).
6		vex	|- x e. _V
7	6	elpw	|- ( x e. ~P A <-> x C_ A )
8	5 7	e2bir	|- (. Tr A ,. x e. A ->. x e. ~P A ).
9	8	in2	|- (. Tr A ->. ( x e. A -> x e. ~P A ) ).
10	9	gen11	|- (. Tr A ->. A. x ( x e. A -> x e. ~P A ) ).
11		biimpr	|- ( ( A C_ ~P A <-> A. x ( x e. A -> x e. ~P A ) ) -> ( A. x ( x e. A -> x e. ~P A ) -> A C_ ~P A ) )
12	1 10 11	e01	|- (. Tr A ->. A C_ ~P A ).
13	12	in1	|- ( Tr A -> A C_ ~P A )