This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 df-ss 
 |-  ( ( _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 )