funsex - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > funsex		Unicode version

Theorem funsex 5829

Description: The class of all functions forms a set. (Contributed by SF, 18-Feb-2015.)

**Assertion**
Ref	Expression
funsex	Funs

Proof of Theorem funsex Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-funs 5761	. . 3 Funs
2		elima1c 4948	. . . . . . . 8 ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c
3		snex 4112	. . . . . . . . . . . 12
4		vex 2863	. . . . . . . . . . . 12
5	3, 4	opex 4589	. . . . . . . . . . 11
6	5	elcompl 3226	. . . . . . . . . 10 ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c
7		elima1c 4948	. . . . . . . . . . . 12 ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c
8		elima1c 4948	. . . . . . . . . . . . . . . 16 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3
9		eldif 3222	. . . . . . . . . . . . . . . . . 18 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S $/\$ Ins3
10		snex 4112	. . . . . . . . . . . . . . . . . . . . 21
11	10	otelins2 5792	. . . . . . . . . . . . . . . . . . . 20 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins4 SI₃ 1_c Ins2 Ins2 S
12		vex 2863	. . . . . . . . . . . . . . . . . . . . . . 23
13		vex 2863	. . . . . . . . . . . . . . . . . . . . . . 23
14	12, 13	opex 4589	. . . . . . . . . . . . . . . . . . . . . 22
15	14, 4	opelssetsn 4761	. . . . . . . . . . . . . . . . . . . . 21 S
16		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ 1_c Ins2 Ins2 Ins4 SI₃ 1_c Ins2 Ins2
17		elin 3220	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins4 SI₃ 1_c Ins2 Ins2 Ins4 SI₃ 1_c $/\$ Ins2 Ins2
18	4	oqelins4 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins4 SI₃ 1_c SI₃ 1_c
19		elima1c 4948	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SI₃ 1_c SI₃
20		oteltxp 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 SI₃ $/\$ SI₃
21		opelcnv 4894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
22		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
23	21, 22	bitr4i 243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
24		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
25	24, 13, 12	otsnelsi3 5806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 SI₃
26		oteltxp 5783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
27		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
28		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
29	27, 28	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
30		ancom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
31	29, 30	bitr2i 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
32	12, 13	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
33	26, 31, 32	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
34	25, 33	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 SI₃
35	23, 34	anbi12ci 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ SI₃ $/\$
36	20, 35	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 SI₃ $/\$
37	36	exbii 1582	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 SI₃ $/\$
38		sneq 3745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
39	38	breq2d 4652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
40	14, 39	ceqsexv 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
41	19, 37, 40	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 SI₃ 1_c
42	18, 41	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins4 SI₃ 1_c
43	3	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2
44		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
45	44	otelins2 5792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Ins2 Ins2 Ins2
46		df-br 4641	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
47	43, 45, 46	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Ins2 Ins2
48	42, 47	anbi12i 678	. . . . . . . . . . . . . . . . . . . . . . . . 25 Ins4 SI₃ 1_c $/\$ Ins2 Ins2 $/\$
49	17, 48	bitri 240	. . . . . . . . . . . . . . . . . . . . . . . 24 Ins4 SI₃ 1_c Ins2 Ins2 $/\$
50		snex 4112	. . . . . . . . . . . . . . . . . . . . . . . . 25
51	50, 4	op1st2nd 5791	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
52	16, 49, 51	3bitri 262	. . . . . . . . . . . . . . . . . . . . . . 23 Ins4 SI₃ 1_c Ins2 Ins2
53	52	rexbii 2640	. . . . . . . . . . . . . . . . . . . . . 22 S Ins4 SI₃ 1_c Ins2 Ins2 S
54		elima 4755	. . . . . . . . . . . . . . . . . . . . . 22 Ins4 SI₃ 1_c Ins2 Ins2 S S Ins4 SI₃ 1_c Ins2 Ins2
55		risset 2662	. . . . . . . . . . . . . . . . . . . . . 22 S S
56	53, 54, 55	3bitr4i 268	. . . . . . . . . . . . . . . . . . . . 21 Ins4 SI₃ 1_c Ins2 Ins2 S S
57		df-br 4641	. . . . . . . . . . . . . . . . . . . . 21
58	15, 56, 57	3bitr4i 268	. . . . . . . . . . . . . . . . . . . 20 Ins4 SI₃ 1_c Ins2 Ins2 S
59	11, 58	bitri 240	. . . . . . . . . . . . . . . . . . 19 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S
60	5	otelins3 5793	. . . . . . . . . . . . . . . . . . . . 21 Ins3
61	10	ideq 4871	. . . . . . . . . . . . . . . . . . . . . 22
62		df-br 4641	. . . . . . . . . . . . . . . . . . . . . 22
63	13	sneqb 3877	. . . . . . . . . . . . . . . . . . . . . 22
64	61, 62, 63	3bitr3i 266	. . . . . . . . . . . . . . . . . . . . 21
65	60, 64	bitri 240	. . . . . . . . . . . . . . . . . . . 20 Ins3
66	65	notbii 287	. . . . . . . . . . . . . . . . . . 19 Ins3
67	59, 66	anbi12i 678	. . . . . . . . . . . . . . . . . 18 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S $/\$ Ins3 $/\$
68	9, 67	bitri 240	. . . . . . . . . . . . . . . . 17 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 $/\$
69	68	exbii 1582	. . . . . . . . . . . . . . . 16 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 $/\$
70	8, 69	bitri 240	. . . . . . . . . . . . . . 15 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c $/\$
71	70	notbii 287	. . . . . . . . . . . . . 14 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c $/\$
72	10, 5	opex 4589	. . . . . . . . . . . . . . 15
73	72	elcompl 3226	. . . . . . . . . . . . . 14 ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c
74		exanali 1585	. . . . . . . . . . . . . . 15 $/\$
75	74	con2bii 322	. . . . . . . . . . . . . 14 $/\$
76	71, 73, 75	3bitr4i 268	. . . . . . . . . . . . 13 ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c
77	76	exbii 1582	. . . . . . . . . . . 12 ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c
78	7, 77	bitri 240	. . . . . . . . . . 11 ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c
79	78	notbii 287	. . . . . . . . . 10 ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c
80	6, 79	bitri 240	. . . . . . . . 9 ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c
81	80	exbii 1582	. . . . . . . 8 ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c
82	2, 81	bitri 240	. . . . . . 7 ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
83	82	notbii 287	. . . . . 6 ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
84	4	elcompl 3226	. . . . . 6 ∼ ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
85		alex 1572	. . . . . 6
86	83, 84, 85	3bitr4i 268	. . . . 5 ∼ ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
87		dffun3 5121	. . . . 5
88	86, 87	bitr4i 243	. . . 4 ∼ ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
89	88	eqabi 2465	. . 3 ∼ ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
90	1, 89	eqtr4i 2376	. 2 Funs ∼ ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
91		1stex 4740	. . . . . . . . . . . . . . . 16
92	91	cnvex 5103	. . . . . . . . . . . . . . 15
93		2ndex 5113	. . . . . . . . . . . . . . . . 17
94	93, 91	txpex 5786	. . . . . . . . . . . . . . . 16
95	94	si3ex 5807	. . . . . . . . . . . . . . 15 SI₃
96	92, 95	txpex 5786	. . . . . . . . . . . . . 14 SI₃
97		1cex 4143	. . . . . . . . . . . . . 14 1_c
98	96, 97	imaex 4748	. . . . . . . . . . . . 13 SI₃ 1_c
99	98	ins4ex 5800	. . . . . . . . . . . 12 Ins4 SI₃ 1_c
100	93	ins2ex 5798	. . . . . . . . . . . . 13 Ins2
101	100	ins2ex 5798	. . . . . . . . . . . 12 Ins2 Ins2
102	99, 101	inex 4106	. . . . . . . . . . 11 Ins4 SI₃ 1_c Ins2 Ins2
103		ssetex 4745	. . . . . . . . . . 11 S
104	102, 103	imaex 4748	. . . . . . . . . 10 Ins4 SI₃ 1_c Ins2 Ins2 S
105	104	ins2ex 5798	. . . . . . . . 9 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S
106		idex 5505	. . . . . . . . . 10
107	106	ins3ex 5799	. . . . . . . . 9 Ins3
108	105, 107	difex 4108	. . . . . . . 8 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3
109	108, 97	imaex 4748	. . . . . . 7 Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c
110	109	complex 4105	. . . . . 6 ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c
111	110, 97	imaex 4748	. . . . 5 ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c
112	111	complex 4105	. . . 4 ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c
113	112, 97	imaex 4748	. . 3 ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
114	113	complex 4105	. 2 ∼ ∼ ∼ Ins2 Ins4 SI₃ 1_c Ins2 Ins2 S Ins3 1_c1_c1_c
115	90, 114	eqeltri 2423	1 Funs

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 358

wal 1540

wex 1541

wceq 1642

wcel 1710

cab 2339

wrex 2616

cvv 2860 ∼ ccompl 3206

cdif 3207

cin 3209

csn 3738 1_cc1c 4135

cop 4562 class class class wbr 4640

c1st 4718 S csset 4720

cima 4723

cid 4764

ccnv 4772

wfun 4776

c2nd 4784

ctxp 5736 Ins2 cins2 5750 Ins3 cins3 5752 Ins4 cins4 5756 SI₃ csi3 5758 Funs cfuns 5760

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-13 1712 ax-14 1714 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-pss 3262 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-fin 4381 df-lefin 4441 df-ltfin 4442 df-ncfin 4443 df-tfin 4444 df-evenfin 4445 df-oddfin 4446 df-sfin 4447 df-spfin 4448 df-phi 4566 df-op 4567 df-proj1 4568 df-proj2 4569 df-opab 4624 df-br 4641 df-1st 4724 df-swap 4725 df-sset 4726 df-co 4727 df-ima 4728 df-si 4729 df-id 4768 df-cnv 4786 df-fun 4790 df-2nd 4798 df-txp 5737 df-ins2 5751 df-ins3 5753 df-ins4 5757 df-si3 5759 df-funs 5761

This theorem is referenced by: fnsex 5833 mapexi 6004 pmex 6006 fnpm 6009

W3C validator