Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Hankins
Refinements
fneref
Next ⟩
fnetr
Metamath Proof Explorer
Ascii
Unicode
Theorem
fneref
Description:
Reflexivity of the fineness relation.
(Contributed by
Jeff Hankins
, 12-Oct-2009)
Ref
Expression
Assertion
fneref
⊢
A
∈
V
→
A
Fne
A
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
⋃
A
=
⋃
A
2
ssid
⊢
x
⊆
x
3
elequ2
⊢
z
=
x
→
y
∈
z
↔
y
∈
x
4
sseq1
⊢
z
=
x
→
z
⊆
x
↔
x
⊆
x
5
3
4
anbi12d
⊢
z
=
x
→
y
∈
z
∧
z
⊆
x
↔
y
∈
x
∧
x
⊆
x
6
5
rspcev
⊢
x
∈
A
∧
y
∈
x
∧
x
⊆
x
→
∃
z
∈
A
y
∈
z
∧
z
⊆
x
7
2
6
mpanr2
⊢
x
∈
A
∧
y
∈
x
→
∃
z
∈
A
y
∈
z
∧
z
⊆
x
8
7
rgen2
⊢
∀
x
∈
A
∀
y
∈
x
∃
z
∈
A
y
∈
z
∧
z
⊆
x
9
1
8
pm3.2i
⊢
⋃
A
=
⋃
A
∧
∀
x
∈
A
∀
y
∈
x
∃
z
∈
A
y
∈
z
∧
z
⊆
x
10
1
1
isfne2
⊢
A
∈
V
→
A
Fne
A
↔
⋃
A
=
⋃
A
∧
∀
x
∈
A
∀
y
∈
x
∃
z
∈
A
y
∈
z
∧
z
⊆
x
11
9
10
mpbiri
⊢
A
∈
V
→
A
Fne
A