re2luk1 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > re2luk1		Structured version Unicode version

Theorem re2luk1 1540

Description: luk-1 1430 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
re2luk1

**Proof of Theorem re2luk1**
Step	Hyp	Ref	Expression
1		rb-imdf 1525	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
2	1	rblem7 1538	. . 3 $\/$ $\/$
3		rb-imdf 1525	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
4	3	rblem6 1537	. . . . . . 7 $\/$ $\/$
5		rb-ax2 1528	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
6		rb-ax4 1530	. . . . . . . . . 10 $\/$ $\/$
7		rb-ax3 1529	. . . . . . . . . 10 $\/$ $\/$
8	6, 7	rbsyl 1531	. . . . . . . . 9 $\/$
9		rb-ax4 1530	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$ $\/$
10		rb-ax3 1529	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$ $\/$
11	9, 10	rbsyl 1531	. . . . . . . . . 10 $\/$ $\/$ $\/$
12		rb-ax2 1528	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
13	11, 12	anmp 1526	. . . . . . . . 9 $\/$ $\/$ $\/$
14	8, 13	rblem1 1532	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$
15	5, 14	rbsyl 1531	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$
16	4, 15	anmp 1526	. . . . . 6 $\/$ $\/$
17		rb-imdf 1525	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$
18	17	rblem7 1538	. . . . . 6 $\/$ $\/$
19	16, 18	rblem1 1532	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
20		rb-ax1 1527	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$
21		rb-ax2 1528	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
22		rb-ax4 1530	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
23		rb-ax3 1529	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
24	22, 23	rbsyl 1531	. . . . . . . . 9 $\/$ $\/$ $\/$
25		rb-ax4 1530	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
26		rb-ax3 1529	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$ $\/$
27	25, 26	rbsyl 1531	. . . . . . . . 9 $\/$ $\/$ $\/$
28	24, 27, 11	rblem4 1535	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
29		rb-ax2 1528	. . . . . . . 8 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
30	28, 29	rbsyl 1531	. . . . . . 7 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
31	21, 30	rbsyl 1531	. . . . . 6 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
32	20, 31	anmp 1526	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
33	19, 32	rbsyl 1531	. . . 4 $\/$ $\/$ $\/$
34		rb-imdf 1525	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$
35	34	rblem6 1537	. . . 4 $\/$ $\/$
36	33, 35	rbsyl 1531	. . 3 $\/$ $\/$
37	2, 36	rbsyl 1531	. 2 $\/$
38		rb-imdf 1525	. . 3 $\/$ $\/$ $\/$ $\/$ $\/$
39	38	rblem7 1538	. 2 $\/$ $\/$
40	37, 39	anmp 1526	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $\/$ wo 359

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362

W3C validator