refref

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

		Ref	Expression
	Assertion	refref	$⊢ A \in V \to A Ref A$

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

Metamath Proof Explorer