Theorem boxcutc 7837

Description: The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015.)

Assertion

Ref	Expression
boxcutc	⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) → (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) = X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵))

Distinct variable groups:   𝐴,𝑘   𝑘,𝑋

Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem boxcutc

Dummy variables 𝑙 𝑚 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 3694	. . 3 ⊢ (𝑧 ∈ (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) → 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵)
2	1	adantl 481	. 2 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵))) → 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵)
3		sseq1 3589	. . . . . 6 ⊢ ((𝐵 ∖ 𝐶) = if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) → ((𝐵 ∖ 𝐶) ⊆ 𝐵 ↔ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ⊆ 𝐵))
4		sseq1 3589	. . . . . 6 ⊢ (𝐵 = if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) → (𝐵 ⊆ 𝐵 ↔ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ⊆ 𝐵))
5		difss 3699	. . . . . 6 ⊢ (𝐵 ∖ 𝐶) ⊆ 𝐵
6		ssid 3587	. . . . . 6 ⊢ 𝐵 ⊆ 𝐵
7	3, 4, 5, 6	keephyp 4102	. . . . 5 ⊢ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ⊆ 𝐵
8	7	rgenw 2908	. . . 4 ⊢ ∀𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ⊆ 𝐵
9		ss2ixp 7807	. . . 4 ⊢ (∀𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ⊆ 𝐵 → X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ⊆ X𝑘 ∈ 𝐴 𝐵)
10	8, 9	mp1i 13	. . 3 ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) → X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ⊆ X𝑘 ∈ 𝐴 𝐵)
11	10	sselda 3568	. 2 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)) → 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵)
12		ixpfn 7800	. . . . . . . . 9 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 → 𝑧 Fn 𝐴)
13	12	adantl 481	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → 𝑧 Fn 𝐴)
14	13	biantrurd 528	. . . . . . 7 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵))))
15		vex 3176	. . . . . . . 8 ⊢ 𝑧 ∈ V
16	15	elixp 7801	. . . . . . 7 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵)))
17	14, 16	syl6rbbr 278	. . . . . 6 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵)))
18	17	notbid 307	. . . . 5 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (¬ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ ¬ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵)))
19		rexnal 2978	. . . . . 6 ⊢ (∃𝑘 ∈ 𝐴 ¬ (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ ¬ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵))
20		eleq2 2677	. . . . . . . . . 10 ⊢ ((⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶) = if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵) → ((𝑧‘𝑚) ∈ (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶) ↔ (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)))
21		eleq2 2677	. . . . . . . . . 10 ⊢ (⦋𝑚 / 𝑘⦌𝐵 = if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵) → ((𝑧‘𝑚) ∈ ⦋𝑚 / 𝑘⦌𝐵 ↔ (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)))
22		eleq2 2677	. . . . . . . . . . . . . . . . . . 19 ⊢ (⦋𝑙 / 𝑘⦌𝐶 = if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) → ((𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐶 ↔ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)))
23		eleq2 2677	. . . . . . . . . . . . . . . . . . 19 ⊢ (⦋𝑙 / 𝑘⦌𝐵 = if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) → ((𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵 ↔ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)))
24		simpl 472	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) → 𝑋 ∈ 𝐴)
25	15	elixp 7801	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ 𝐵))
26	25	simprbi 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 → ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ 𝐵)
27		nfv 1830	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑙(𝑧‘𝑘) ∈ 𝐵
28		nfcsb1v 3515	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑘⦋𝑙 / 𝑘⦌𝐵
29	28	nfel2 2767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑘(𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵
30		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑙 → (𝑧‘𝑘) = (𝑧‘𝑙))
31		csbeq1a 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = 𝑙 → 𝐵 = ⦋𝑙 / 𝑘⦌𝐵)
32	30, 31	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑘 = 𝑙 → ((𝑧‘𝑘) ∈ 𝐵 ↔ (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵))
33	27, 29, 32	cbvral 3143	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ 𝐵 ↔ ∀𝑙 ∈ 𝐴 (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵)
34	26, 33	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 → ∀𝑙 ∈ 𝐴 (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵)
35		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑙 = 𝑋 → (𝑧‘𝑙) = (𝑧‘𝑋))
36		csbeq1 3502	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑙 = 𝑋 → ⦋𝑙 / 𝑘⦌𝐵 = ⦋𝑋 / 𝑘⦌𝐵)
37	35, 36	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = 𝑋 → ((𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵 ↔ (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐵))
38	37	rspcva 3280	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑙 ∈ 𝐴 (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵) → (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐵)
39	24, 34, 38	syl2an 493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐵)
40		neldif 3697	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐵 ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) → (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐶)
41	39, 40	sylan 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) → (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐶)
42	41	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) ∧ 𝑙 ∈ 𝐴) → (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐶)
43		csbeq1 3502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑙 = 𝑋 → ⦋𝑙 / 𝑘⦌𝐶 = ⦋𝑋 / 𝑘⦌𝐶)
44	35, 43	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑙 = 𝑋 → ((𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐶 ↔ (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐶))
45	42, 44	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) ∧ 𝑙 ∈ 𝐴) → (𝑙 = 𝑋 → (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐶))
46	45	imp 444	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) ∧ 𝑙 ∈ 𝐴) ∧ 𝑙 = 𝑋) → (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐶)
47	34	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) → ∀𝑙 ∈ 𝐴 (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵)
48	47	r19.21bi 2916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) ∧ 𝑙 ∈ 𝐴) → (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵)
49	48	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) ∧ 𝑙 ∈ 𝐴) ∧ ¬ 𝑙 = 𝑋) → (𝑧‘𝑙) ∈ ⦋𝑙 / 𝑘⦌𝐵)
50	22, 23, 46, 49	ifbothda 4073	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) ∧ 𝑙 ∈ 𝐴) → (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵))
51	50	ralrimiva 2949	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) → ∀𝑙 ∈ 𝐴 (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵))
52		dfral2 2977	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑙 ∈ 𝐴 (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) ↔ ¬ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵))
53	51, 52	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)) → ¬ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵))
54	53	ex 449	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (¬ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶) → ¬ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)))
55	54	con4d 113	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) → (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)))
56	55	imp 444	. . . . . . . . . . . . 13 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) → (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶))
57	56	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) ∧ 𝑚 ∈ 𝐴) → (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶))
58		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑋 → (𝑧‘𝑚) = (𝑧‘𝑋))
59		csbeq1 3502	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑋 → ⦋𝑚 / 𝑘⦌𝐵 = ⦋𝑋 / 𝑘⦌𝐵)
60		csbeq1 3502	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑋 → ⦋𝑚 / 𝑘⦌𝐶 = ⦋𝑋 / 𝑘⦌𝐶)
61	59, 60	difeq12d 3691	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑋 → (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶) = (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶))
62	58, 61	eleq12d 2682	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑋 → ((𝑧‘𝑚) ∈ (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶) ↔ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)))
63	57, 62	syl5ibrcom 236	. . . . . . . . . . 11 ⊢ (((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) ∧ 𝑚 ∈ 𝐴) → (𝑚 = 𝑋 → (𝑧‘𝑚) ∈ (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶)))
64	63	imp 444	. . . . . . . . . 10 ⊢ ((((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) ∧ 𝑚 ∈ 𝐴) ∧ 𝑚 = 𝑋) → (𝑧‘𝑚) ∈ (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶))
65		nfv 1830	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑚(𝑧‘𝑘) ∈ 𝐵
66		nfcsb1v 3515	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐵
67	66	nfel2 2767	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘(𝑧‘𝑚) ∈ ⦋𝑚 / 𝑘⦌𝐵
68		fveq2 6103	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑚 → (𝑧‘𝑘) = (𝑧‘𝑚))
69		csbeq1a 3508	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑚 → 𝐵 = ⦋𝑚 / 𝑘⦌𝐵)
70	68, 69	eleq12d 2682	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑚 → ((𝑧‘𝑘) ∈ 𝐵 ↔ (𝑧‘𝑚) ∈ ⦋𝑚 / 𝑘⦌𝐵))
71	65, 67, 70	cbvral 3143	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ 𝐵 ↔ ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ ⦋𝑚 / 𝑘⦌𝐵)
72	26, 71	sylib 207	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 → ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ ⦋𝑚 / 𝑘⦌𝐵)
73	72	ad2antlr 759	. . . . . . . . . . . 12 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) → ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ ⦋𝑚 / 𝑘⦌𝐵)
74	73	r19.21bi 2916	. . . . . . . . . . 11 ⊢ (((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) ∧ 𝑚 ∈ 𝐴) → (𝑧‘𝑚) ∈ ⦋𝑚 / 𝑘⦌𝐵)
75	74	adantr 480	. . . . . . . . . 10 ⊢ ((((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) ∧ 𝑚 ∈ 𝐴) ∧ ¬ 𝑚 = 𝑋) → (𝑧‘𝑚) ∈ ⦋𝑚 / 𝑘⦌𝐵)
76	20, 21, 64, 75	ifbothda 4073	. . . . . . . . 9 ⊢ (((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) ∧ 𝑚 ∈ 𝐴) → (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵))
77	76	ralrimiva 2949	. . . . . . . 8 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)) → ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵))
78		simplll 794	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)) → 𝑋 ∈ 𝐴)
79		simpll 786	. . . . . . . . . . 11 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → 𝑋 ∈ 𝐴)
80		iftrue 4042	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑋 → if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵) = (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶))
81	80, 61	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑋 → if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵) = (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶))
82	58, 81	eleq12d 2682	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑋 → ((𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵) ↔ (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶)))
83	82	rspcva 3280	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)) → (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶))
84	79, 83	sylan 487	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)) → (𝑧‘𝑋) ∈ (⦋𝑋 / 𝑘⦌𝐵 ∖ ⦋𝑋 / 𝑘⦌𝐶))
85	84	eldifbd 3553	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)) → ¬ (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐶)
86		iftrue 4042	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑋 → if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) = ⦋𝑙 / 𝑘⦌𝐶)
87	86, 43	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑋 → if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) = ⦋𝑋 / 𝑘⦌𝐶)
88	35, 87	eleq12d 2682	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑋 → ((𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) ↔ (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐶))
89	88	notbid 307	. . . . . . . . . 10 ⊢ (𝑙 = 𝑋 → (¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) ↔ ¬ (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐶))
90	89	rspcev 3282	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ ¬ (𝑧‘𝑋) ∈ ⦋𝑋 / 𝑘⦌𝐶) → ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵))
91	78, 85, 90	syl2anc 691	. . . . . . . 8 ⊢ ((((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) ∧ ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)) → ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵))
92	77, 91	impbida 873	. . . . . . 7 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵) ↔ ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)))
93		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑙 ¬ (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵)
94		nfv 1830	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 𝑙 = 𝑋
95		nfcsb1v 3515	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑙 / 𝑘⦌𝐶
96	94, 95, 28	nfif 4065	. . . . . . . . . 10 ⊢ Ⅎ𝑘if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)
97	96	nfel2 2767	. . . . . . . . 9 ⊢ Ⅎ𝑘(𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)
98	97	nfn 1768	. . . . . . . 8 ⊢ Ⅎ𝑘 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)
99		eqeq1 2614	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → (𝑘 = 𝑋 ↔ 𝑙 = 𝑋))
100		csbeq1a 3508	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → 𝐶 = ⦋𝑙 / 𝑘⦌𝐶)
101	99, 100, 31	ifbieq12d 4063	. . . . . . . . . 10 ⊢ (𝑘 = 𝑙 → if(𝑘 = 𝑋, 𝐶, 𝐵) = if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵))
102	30, 101	eleq12d 2682	. . . . . . . . 9 ⊢ (𝑘 = 𝑙 → ((𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)))
103	102	notbid 307	. . . . . . . 8 ⊢ (𝑘 = 𝑙 → (¬ (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵)))
104	93, 98, 103	cbvrex 3144	. . . . . . 7 ⊢ (∃𝑘 ∈ 𝐴 ¬ (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ ∃𝑙 ∈ 𝐴 ¬ (𝑧‘𝑙) ∈ if(𝑙 = 𝑋, ⦋𝑙 / 𝑘⦌𝐶, ⦋𝑙 / 𝑘⦌𝐵))
105		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑚(𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)
106		nfv 1830	. . . . . . . . . 10 ⊢ Ⅎ𝑘 𝑚 = 𝑋
107		nfcsb1v 3515	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋𝑚 / 𝑘⦌𝐶
108	66, 107	nfdif 3693	. . . . . . . . . 10 ⊢ Ⅎ𝑘(⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶)
109	106, 108, 66	nfif 4065	. . . . . . . . 9 ⊢ Ⅎ𝑘if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)
110	109	nfel2 2767	. . . . . . . 8 ⊢ Ⅎ𝑘(𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)
111		eqeq1 2614	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → (𝑘 = 𝑋 ↔ 𝑚 = 𝑋))
112		csbeq1a 3508	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑚 → 𝐶 = ⦋𝑚 / 𝑘⦌𝐶)
113	69, 112	difeq12d 3691	. . . . . . . . . 10 ⊢ (𝑘 = 𝑚 → (𝐵 ∖ 𝐶) = (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶))
114	111, 113, 69	ifbieq12d 4063	. . . . . . . . 9 ⊢ (𝑘 = 𝑚 → if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) = if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵))
115	68, 114	eleq12d 2682	. . . . . . . 8 ⊢ (𝑘 = 𝑚 → ((𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ↔ (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵)))
116	105, 110, 115	cbvral 3143	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ↔ ∀𝑚 ∈ 𝐴 (𝑧‘𝑚) ∈ if(𝑚 = 𝑋, (⦋𝑚 / 𝑘⦌𝐵 ∖ ⦋𝑚 / 𝑘⦌𝐶), ⦋𝑚 / 𝑘⦌𝐵))
117	92, 104, 116	3bitr4g 302	. . . . . 6 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (∃𝑘 ∈ 𝐴 ¬ (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)))
118	19, 117	syl5bbr 273	. . . . 5 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (¬ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)))
119	18, 118	bitrd 267	. . . 4 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (¬ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)))
120		ibar 524	. . . . 5 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 → (¬ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 ∧ ¬ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵))))
121	120	adantl 481	. . . 4 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (¬ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵) ↔ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 ∧ ¬ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵))))
122	13	biantrurd 528	. . . 4 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵))))
123	119, 121, 122	3bitr3d 297	. . 3 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → ((𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 ∧ ¬ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵))))
124		eldif 3550	. . 3 ⊢ (𝑧 ∈ (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) ↔ (𝑧 ∈ X𝑘 ∈ 𝐴 𝐵 ∧ ¬ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)))
125	15	elixp 7801	. . 3 ⊢ (𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑧‘𝑘) ∈ if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)))
126	123, 124, 125	3bitr4g 302	. 2 ⊢ (((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) ∧ 𝑧 ∈ X𝑘 ∈ 𝐴 𝐵) → (𝑧 ∈ (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) ↔ 𝑧 ∈ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵)))
127	2, 11, 126	eqrdav 2609	1 ⊢ ((𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵) → (X𝑘 ∈ 𝐴 𝐵 ∖ X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, 𝐶, 𝐵)) = X𝑘 ∈ 𝐴 if(𝑘 = 𝑋, (𝐵 ∖ 𝐶), 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ⦋csb 3499   ∖ cdif 3537   ⊆ wss 3540  ifcif 4036   Fn wfn 5799  ‘cfv 5804  Xcixp 7794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-ixp 7795

This theorem is referenced by:  ptcld  21226