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 )