Theorem refref

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

	Ref	Expression
Assertion	refref	$$⊢A\in V\to A\mathrm{Ref}A$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\bigcup A=\bigcup A$$
2		ssid	$$⊢x\subseteq x$$
3		sseq2	$$⊢y=x\to \left(x\subseteq y\leftrightarrow x\subseteq x\right)$$
4	3	rspcev	$$⊢\left(x\in A\wedge x\subseteq x\right)\to \exists y\in Ax\subseteq y$$
5	2 4	mpan2	$$⊢x\in A\to \exists y\in Ax\subseteq y$$
6	5	rgen	$$⊢\forall x\in A\exists y\in Ax\subseteq y$$
7	1 6	pm3.2i	$$⊢\left(\bigcup A=\bigcup A\wedge \forall x\in A\exists y\in Ax\subseteq y\right)$$
8	1 1	isref	$$⊢A\in V\to \left(A\mathrm{Ref}A\leftrightarrow \left(\bigcup A=\bigcup A\wedge \forall x\in A\exists y\in Ax\subseteq y\right)\right)$$
9	7 8	mpbiri	$$⊢A\in V\to A\mathrm{Ref}A$$