Theorem idref 6170

Description: TODO: This is the same as issref 5231 (which has a much longer proof). Should we replace issref 5231 with this one? - NM 9-May-2016.

Two ways to state a relation is reflexive. (Adapted from Tarski.) (Contributed by FL, 15-Jan-2012.) (Proof shortened by Mario Carneiro, 3-Nov-2015.) (Proof modification is discouraged.)

Assertion

Ref	Expression
idref	|- ( ( _I |` A ) C_ R <-> A. x e. A x R x )

Distinct variable groups:   x, A   x, R

Proof of Theorem idref

Step	Hyp	Ref	Expression
1		eqid 2461	. . . 4 |- ( x e. A |-> <. x , x >. ) = ( x e. A |-> <. x , x >. )
2	1	fmpt 6065	. . 3 |- ( A. x e. A <. x , x >. e. R <-> ( x e. A |-> <. x , x >. ) : A --> R )
3		opex 4677	. . . . 5 |- <. x , x >. e. _V
4	3, 1	fnmpti 5727	. . . 4 |- ( x e. A |-> <. x , x >. ) Fn A
5		df-f 5604	. . . 4 |- ( ( x e. A |-> <. x , x >. ) : A --> R <-> ( ( x e. A |-> <. x , x >. ) Fn A /\ ran ( x e. A |-> <. x , x >. ) C_ R ) )
6	4, 5	mpbiran 934	. . 3 |- ( ( x e. A |-> <. x , x >. ) : A --> R <-> ran ( x e. A |-> <. x , x >. ) C_ R )
7	2, 6	bitri 257	. 2 |- ( A. x e. A <. x , x >. e. R <-> ran ( x e. A |-> <. x , x >. ) C_ R )
8		df-br 4416	. . 3 |- ( x R x <-> <. x , x >. e. R )
9	8	ralbii 2830	. 2 |- ( A. x e. A x R x <-> A. x e. A <. x , x >. e. R )
10		mptresid 5177	. . . 4 |- ( x e. A |-> x ) = ( _I |` A )
11		vex 3059	. . . . 5 |- x e. _V
12	11	fnasrn 6093	. . . 4 |- ( x e. A |-> x ) = ran ( x e. A |-> <. x , x >. )
13	10, 12	eqtr3i 2485	. . 3 |- ( _I |` A ) = ran ( x e. A |-> <. x , x >. )
14	13	sseq1i 3467	. 2 |- ( ( _I |` A ) C_ R <-> ran ( x e. A |-> <. x , x >. ) C_ R )
15	7, 9, 14	3bitr4ri 286	1 |- ( ( _I |` A ) C_ R <-> A. x e. A x R x )

Syntax hints:   <-> wb 189   e. wcel 1897   A.wral 2748   C_ wss 3415   <.cop 3985   class class class wbr 4415   |-> cmpt 4474   _I cid 4762   ran crn 4853   |` cres 4854   Fn wfn 5595   -->wf 5596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608

This theorem is referenced by:  retos  19234  filnetlem2  31083