Metamath Proof Explorer


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