Metamath Proof Explorer

Theorem fneref

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

Ref Expression
Assertion fneref 
|- ( A e. V -> A Fne A )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. A = U. A
2 ssid 
 |-  x C_ x
3 elequ2 
 |-  ( z = x -> ( y e. z <-> y e. x ) )
4 sseq1 
 |-  ( z = x -> ( z C_ x <-> x C_ x ) )
5 3 4 anbi12d 
 |-  ( z = x -> ( ( y e. z /\ z C_ x ) <-> ( y e. x /\ x C_ x ) ) )
6 5 rspcev 
 |-  ( ( x e. A /\ ( y e. x /\ x C_ x ) ) -> E. z e. A ( y e. z /\ z C_ x ) )
7 2 6 mpanr2 
 |-  ( ( x e. A /\ y e. x ) -> E. z e. A ( y e. z /\ z C_ x ) )
8 7 rgen2 
 |-  A. x e. A A. y e. x E. z e. A ( y e. z /\ z C_ x )
9 1 8 pm3.2i 
 |-  ( U. A = U. A /\ A. x e. A A. y e. x E. z e. A ( y e. z /\ z C_ x ) )
10 1 1 isfne2 
 |-  ( A e. V -> ( A Fne A <-> ( U. A = U. A /\ A. x e. A A. y e. x E. z e. A ( y e. z /\ z C_ x ) ) ) )
11 9 10 mpbiri 
 |-  ( A e. V -> A Fne A )