Metamath Proof Explorer


Theorem idref

Description: Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012) (Proof shortened by Mario Carneiro, 3-Nov-2015) (Revised by NM, 30-Mar-2016)

Ref Expression
Assertion idref I A R x A x R x

Proof

Step Hyp Ref Expression
1 eqid x A x x = x A x x
2 1 fmpt x A x x R x A x x : A R
3 opex x x V
4 3 1 fnmpti x A x x Fn A
5 df-f x A x x : A R x A x x Fn A ran x A x x R
6 4 5 mpbiran x A x x : A R ran x A x x R
7 2 6 bitri x A x x R ran x A x x R
8 df-br x R x x x R
9 8 ralbii x A x R x x A x x R
10 mptresid I A = x A x
11 vex x V
12 11 fnasrn x A x = ran x A x x
13 10 12 eqtri I A = ran x A x x
14 13 sseq1i I A R ran x A x x R
15 7 9 14 3bitr4ri I A R x A x R x