Theorem refref

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

	Ref	Expression
Assertion	refref	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 Ref 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐴 = ∪ 𝐴
2		ssid	⊢ 𝑥 ⊆ 𝑥
3		sseq2	⊢ ( 𝑦 = 𝑥 → ( 𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑥 ) )
4	3	rspcev	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ⊆ 𝑥 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
5	2 4	mpan2	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
6	5	rgen	⊢ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦
7	1 6	pm3.2i	⊢ ( ∪ 𝐴 = ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 )
8	1 1	isref	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 Ref 𝐴 ↔ ( ∪ 𝐴 = ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ 𝑦 ) ) )
9	7 8	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 Ref 𝐴 )