Metamath Proof Explorer


Theorem idrefALT

Description: Alternate proof of idref not relying on definitions related to functions. 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) (Proof shortened by BJ, 28-Aug-2022) The "proof modification is discouraged" tag is here only because this is an *ALT result. (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion idrefALT I A R x A x R x

Proof

Step Hyp Ref Expression
1 dfss2 I A R y y I A y R
2 elrid y I A x A y = x x
3 2 imbi1i y I A y R x A y = x x y R
4 r19.23v x A y = x x y R x A y = x x y R
5 eleq1 y = x x y R x x R
6 df-br x R x x x R
7 5 6 bitr4di y = x x y R x R x
8 7 pm5.74i y = x x y R y = x x x R x
9 8 ralbii x A y = x x y R x A y = x x x R x
10 3 4 9 3bitr2i y I A y R x A y = x x x R x
11 10 albii y y I A y R y x A y = x x x R x
12 ralcom4 x A y y = x x x R x y x A y = x x x R x
13 opex x x V
14 biidd y = x x x R x x R x
15 13 14 ceqsalv y y = x x x R x x R x
16 15 ralbii x A y y = x x x R x x A x R x
17 11 12 16 3bitr2i y y I A y R x A x R x
18 1 17 bitri I A R x A x R x