Theorem issref 5385

Description: Two ways to state a relation is reflexive. Adapted from Tarski. (Contributed by FL, 15-Jan-2012.) (Revised by NM, 30-Mar-2016.)

Assertion

Ref	Expression
issref

Distinct variable groups:   ,   ,

Proof of Theorem issref

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ral 2812	. 2
2		vex 3112	. . . . 5
3		opelresi 5290	. . . . 5
4	2, 3	ax-mp 5	. . . 4
5		df-br 4453	. . . . 5
6	5	bicomi 202	. . . 4
7	4, 6	imbi12i 326	. . 3
8	7	albii 1640	. 2
9		ralidm 3933	. . . . . 6
10		ralv 3123	. . . . . 6
11	9, 10	bitri 249	. . . . 5
12		df-ral 2812	. . . . . . . . 9
13		pm2.27 39	. . . . . . . . . . . 12
14		opelresg 5286	. . . . . . . . . . . . . . 15
15		df-br 4453	. . . . . . . . . . . . . . . . 17
16		vex 3112	. . . . . . . . . . . . . . . . . . 19
17	16	ideq 5160	. . . . . . . . . . . . . . . . . 18
18		opelresi 5290	. . . . . . . . . . . . . . . . . . . . 21
19		pm2.27 39	. . . . . . . . . . . . . . . . . . . . . 22
20		opeq2 4218	. . . . . . . . . . . . . . . . . . . . . . . 24
21	20	eleq1d 2526	. . . . . . . . . . . . . . . . . . . . . . 23
22	21	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . 22
23	19, 22	syl6 33	. . . . . . . . . . . . . . . . . . . . 21
24	18, 23	syl6bir 229	. . . . . . . . . . . . . . . . . . . 20
25	24	pm2.43i 47	. . . . . . . . . . . . . . . . . . 19
26	25	com3r 79	. . . . . . . . . . . . . . . . . 18
27	17, 26	sylbi 195	. . . . . . . . . . . . . . . . 17
28	15, 27	sylbir 213	. . . . . . . . . . . . . . . 16
29	28	imp 429	. . . . . . . . . . . . . . 15
30	14, 29	syl6bi 228	. . . . . . . . . . . . . 14
31	30	com3r 79	. . . . . . . . . . . . 13
32	31	ralrimiv 2869	. . . . . . . . . . . 12
33	13, 32	syl6 33	. . . . . . . . . . 11
34	2, 33	ax-mp 5	. . . . . . . . . 10
35	34	sps 1865	. . . . . . . . 9
36	12, 35	sylbi 195	. . . . . . . 8
37	36	ralimi 2850	. . . . . . 7
38		eleq1 2529	. . . . . . . . 9
39		eleq1 2529	. . . . . . . . 9
40	38, 39	imbi12d 320	. . . . . . . 8
41	40	ralxp 5149	. . . . . . 7
42	37, 41	sylibr 212	. . . . . 6
43		df-ral 2812	. . . . . . 7
44		relres 5306	. . . . . . . . . . . 12
45		df-rel 5011	. . . . . . . . . . . 12
46	44, 45	mpbi 208	. . . . . . . . . . 11
47	46	sseli 3499	. . . . . . . . . 10
48	47	ancri 552	. . . . . . . . 9
49		pm3.31 445	. . . . . . . . 9
50	48, 49	syl5 32	. . . . . . . 8
51	50	alimi 1633	. . . . . . 7
52	43, 51	sylbi 195	. . . . . 6
53	42, 52	syl 16	. . . . 5
54	11, 53	sylbir 213	. . . 4
55		dfss2 3492	. . . 4
56	54, 55	sylibr 212	. . 3
57		ssel 3497	. . . 4
58	57	alrimiv 1719	. . 3
59	56, 58	impbii 188	. 2
60	1, 8, 59	3bitr2ri 274	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  A.wral 2807  cvv 3109  C_wss 3475  <.cop 4035   class class class wbr 4452  cid 4795  X.cxp 5002  |`cres 5006  Relwrel 5009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-iun 4332  df-br 4453  df-opab 4511  df-id 4800  df-xp 5010  df-rel 5011  df-res 5016