fneref

Description: Reflexivity of the fineness relation. (Contributed by Jeff Hankins, 12-Oct-2009)

		Ref	Expression
	Assertion	fneref	$⊢ A \in V \to A Fne A$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃ A = ⋃ A$
2		ssid	$⊢ x \subseteq x$
3		elequ2	$⊢ z = x \to (y \in z \leftrightarrow y \in x)$
4		sseq1	$⊢ z = x \to (z \subseteq x \leftrightarrow x \subseteq x)$
5	3 4	anbi12d	$⊢ z = x \to ((y \in z \land z \subseteq x) \leftrightarrow (y \in x \land x \subseteq x))$
6	5	rspcev	$⊢ (x \in A \land (y \in x \land x \subseteq x)) \to \exists z \in A (y \in z \land z \subseteq x)$
7	2 6	mpanr2	$⊢ (x \in A \land y \in x) \to \exists z \in A (y \in z \land z \subseteq x)$
8	7	rgen2	$⊢ \forall x \in A \forall y \in x \exists z \in A (y \in z \land z \subseteq x)$
9	1 8	pm3.2i	$⊢ (⋃ A = ⋃ A \land \forall x \in A \forall y \in x \exists z \in A (y \in z \land z \subseteq x))$
10	1 1	isfne2	$⊢ A \in V \to (A Fne A \leftrightarrow (⋃ A = ⋃ A \land \forall x \in A \forall y \in x \exists z \in A (y \in z \land z \subseteq x)))$
11	9 10	mpbiri	$⊢ A \in V \to A Fne A$

Metamath Proof Explorer