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 ) C_ R <-> A. x e. A x R x )

Proof

Step Hyp Ref Expression
1 dfss2
 |-  ( ( _I |` A ) C_ R <-> A. y ( y e. ( _I |` A ) -> y e. R ) )
2 elrid
 |-  ( y e. ( _I |` A ) <-> E. x e. A y = <. x , x >. )
3 2 imbi1i
 |-  ( ( y e. ( _I |` A ) -> y e. R ) <-> ( E. x e. A y = <. x , x >. -> y e. R ) )
4 r19.23v
 |-  ( A. x e. A ( y = <. x , x >. -> y e. R ) <-> ( E. x e. A y = <. x , x >. -> y e. R ) )
5 eleq1
 |-  ( y = <. x , x >. -> ( y e. R <-> <. x , x >. e. R ) )
6 df-br
 |-  ( x R x <-> <. x , x >. e. R )
7 5 6 bitr4di
 |-  ( y = <. x , x >. -> ( y e. R <-> x R x ) )
8 7 pm5.74i
 |-  ( ( y = <. x , x >. -> y e. R ) <-> ( y = <. x , x >. -> x R x ) )
9 8 ralbii
 |-  ( A. x e. A ( y = <. x , x >. -> y e. R ) <-> A. x e. A ( y = <. x , x >. -> x R x ) )
10 3 4 9 3bitr2i
 |-  ( ( y e. ( _I |` A ) -> y e. R ) <-> A. x e. A ( y = <. x , x >. -> x R x ) )
11 10 albii
 |-  ( A. y ( y e. ( _I |` A ) -> y e. R ) <-> A. y A. x e. A ( y = <. x , x >. -> x R x ) )
12 ralcom4
 |-  ( A. x e. A A. y ( y = <. x , x >. -> x R x ) <-> A. y A. x e. A ( y = <. x , x >. -> x R x ) )
13 opex
 |-  <. x , x >. e. _V
14 biidd
 |-  ( y = <. x , x >. -> ( x R x <-> x R x ) )
15 13 14 ceqsalv
 |-  ( A. y ( y = <. x , x >. -> x R x ) <-> x R x )
16 15 ralbii
 |-  ( A. x e. A A. y ( y = <. x , x >. -> x R x ) <-> A. x e. A x R x )
17 11 12 16 3bitr2i
 |-  ( A. y ( y e. ( _I |` A ) -> y e. R ) <-> A. x e. A x R x )
18 1 17 bitri
 |-  ( ( _I |` A ) C_ R <-> A. x e. A x R x )