imadif - New Foundations Explorer

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

Theorem imadif 5171

Description: The image of a difference is the difference of images. (Contributed by NM, 24-May-1998.)

**Assertion**
Ref	Expression
imadif

Proof of Theorem imadif Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		anandir 802	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
2	1	exbii 1582	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
3		19.40 1609	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4	2, 3	sylbi 187	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
5		nfv 1619	. . . . . . . . . 10
6		nfe1 1732	. . . . . . . . . 10 $/\$
7	5, 6	nfan 1824	. . . . . . . . 9 $/\$ $/\$
8		funmo 5125	. . . . . . . . . . . . 13
9		brcnv 4892	. . . . . . . . . . . . . 14
10	9	mobii 2240	. . . . . . . . . . . . 13
11	8, 10	sylib 188	. . . . . . . . . . . 12
12		mopick 2266	. . . . . . . . . . . 12 $/\$ $/\$
13	11, 12	sylan 457	. . . . . . . . . . 11 $/\$ $/\$
14	13	con2d 107	. . . . . . . . . 10 $/\$ $/\$
15		imnan 411	. . . . . . . . . 10 $/\$
16	14, 15	sylib 188	. . . . . . . . 9 $/\$ $/\$ $/\$
17	7, 16	alrimi 1765	. . . . . . . 8 $/\$ $/\$ $/\$
18	17	ex 423	. . . . . . 7 $/\$ $/\$
19		exancom 1586	. . . . . . 7 $/\$ $/\$
20		alnex 1543	. . . . . . 7 $/\$ $/\$
21	18, 19, 20	3imtr3g 260	. . . . . 6 $/\$ $/\$
22	21	anim2d 548	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23	4, 22	syl5 28	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
24		19.29r 1597	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	20, 24	sylan2br 462	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26		andi 837	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
27		ianor 474	. . . . . . . 8 $/\$ $\/$
28	27	anbi2i 675	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
29		an32 773	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
30		pm3.24 852	. . . . . . . . . . 11 $/\$
31	30	intnan 880	. . . . . . . . . 10 $/\$ $/\$
32		anass 630	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
33	31, 32	mtbir 290	. . . . . . . . 9 $/\$ $/\$
34	33	biorfi 396	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
35	29, 34	bitri 240	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
36	26, 28, 35	3bitr4i 268	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	exbii 1582	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
38	25, 37	sylib 188	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
39	23, 38	impbid1 194	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
40		elima2 4755	. . . 4 $/\$
41		eldif 3221	. . . . . 6 $/\$
42	41	anbi1i 676	. . . . 5 $/\$ $/\$ $/\$
43	42	exbii 1582	. . . 4 $/\$ $/\$ $/\$
44	40, 43	bitri 240	. . 3 $/\$ $/\$
45		eldif 3221	. . . 4 $/\$
46		elima2 4755	. . . . 5 $/\$
47		elima2 4755	. . . . . 6 $/\$
48	47	notbii 287	. . . . 5 $/\$
49	46, 48	anbi12i 678	. . . 4 $/\$ $/\$ $/\$ $/\$
50	45, 49	bitri 240	. . 3 $/\$ $/\$ $/\$
51	39, 44, 50	3bitr4g 279	. 2
52	51	eqrdv 2351	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 357 $/\$ wa 358

wal 1540

wex 1541

wceq 1642

wcel 1710

wmo 2205

cdif 3206 class class class wbr 4639

cima 4722

ccnv 4771

wfun 4775

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 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 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-ins2 4084 ax-ins3 4085 ax-typlower 4086 ax-sn 4087

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 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-reu 2621 df-rmo 2622 df-rab 2623 df-v 2861 df-sbc 3047 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-pss 3261 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-idk 4195 df-iota 4339 df-0c 4377 df-addc 4378 df-nnc 4379 df-fin 4380 df-lefin 4440 df-ltfin 4441 df-ncfin 4442 df-tfin 4443 df-evenfin 4444 df-oddfin 4445 df-sfin 4446 df-spfin 4447 df-phi 4565 df-op 4566 df-proj1 4567 df-proj2 4568 df-opab 4623 df-br 4640 df-co 4726 df-ima 4727 df-id 4767 df-cnv 4785 df-fun 4789

This theorem is referenced by: imain 5172 resdif 5306

W3C validator