Theorem refref

Description: Reflexivity of refinement. (Contributed by Jeff Hankins, 18-Jan-2010)

	Ref	Expression
Assertion	refref	|- ( A e. V -> A Ref A )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- U. A = U. A
2		ssid	|- x C_ x
3		sseq2	|- ( y = x -> ( x C_ y <-> x C_ x ) )
4	3	rspcev	|- ( ( x e. A /\ x C_ x ) -> E. y e. A x C_ y )
5	2 4	mpan2	|- ( x e. A -> E. y e. A x C_ y )
6	5	rgen	|- A. x e. A E. y e. A x C_ y
7	1 6	pm3.2i	|- ( U. A = U. A /\ A. x e. A E. y e. A x C_ y )
8	1 1	isref	|- ( A e. V -> ( A Ref A <-> ( U. A = U. A /\ A. x e. A E. y e. A x C_ y ) ) )
9	7 8	mpbiri	|- ( A e. V -> A Ref A )