imagekeq - New Foundations Explorer

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

Theorem imagekeq 4245

Description: Equality theorem for image operation. (Contributed by SF, 12-Jan-2015.)

**Assertion**
Ref	Expression
imagekeq	⊢ (A = B → Image_kA = Image_kB)

**Proof of Theorem imagekeq**
Step	Hyp	Ref	Expression
1		sikeq 4242	. . . . . . . 8 ⊢ (A = B → SI_k A = SI_k B)
2	1	cnvkeqd 4218	. . . . . . 7 ⊢ (A = B → ^◡_k SI_k A = ^◡_k SI_k B)
3	2	cokeq2d 4236	. . . . . 6 ⊢ (A = B → ( S_k ∘_k ^◡_k SI_k A) = ( S_k ∘_k ^◡_k SI_k B))
4	3	ins3keqd 4224	. . . . 5 ⊢ (A = B → Ins3_k ( S_k ∘_k ^◡_k SI_k A) = Ins3_k ( S_k ∘_k ^◡_k SI_k B))
5	4	symdifeq2d 3256	. . . 4 ⊢ (A = B → ( Ins2_k S_k ⊕ Ins3_k ( S_k ∘_k ^◡_k SI_k A)) = ( Ins2_k S_k ⊕ Ins3_k ( S_k ∘_k ^◡_k SI_k B)))
6	5	imakeq1d 4229	. . 3 ⊢ (A = B → (( Ins2_k S_k ⊕ Ins3_k ( S_k ∘_k ^◡_k SI_k A)) “_k ℘₁℘₁1_c) = (( Ins2_k S_k ⊕ Ins3_k ( S_k ∘_k ^◡_k SI_k B)) “_k ℘₁℘₁1_c))
7	6	difeq2d 3386	. 2 ⊢ (A = B → ((V ×_k V) ∖ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∘_k ^◡_k SI_k A)) “_k ℘₁℘₁1_c)) = ((V ×_k V) ∖ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∘_k ^◡_k SI_k B)) “_k ℘₁℘₁1_c)))
8		df-imagek 4195	. 2 ⊢ Image_kA = ((V ×_k V) ∖ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∘_k ^◡_k SI_k A)) “_k ℘₁℘₁1_c))
9		df-imagek 4195	. 2 ⊢ Image_kB = ((V ×_k V) ∖ (( Ins2_k S_k ⊕ Ins3_k ( S_k ∘_k ^◡_k SI_k B)) “_k ℘₁℘₁1_c))
10	7, 8, 9	3eqtr4g 2410	1 ⊢ (A = B → Image_kA = Image_kB)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1642 Vcvv 2860 ∖ cdif 3207 ⊕ csymdif 3210 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 ^◡_kccnvk 4176 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 ∘_k ccomk 4181 SI_k csik 4182 Image_kcimagek 4183 S_k cssetk 4184

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-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-rex 2621 df-v 2862 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-cnvk 4187 df-ins3k 4189 df-imak 4190 df-cok 4191 df-sik 4193 df-imagek 4195

This theorem is referenced by: (None)

W3C validator