Theorem boxcutc

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

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

Proof

Step	Hyp	Ref	Expression
1		eldifi	⊢ ( 𝑧 ∈ ( X 𝑘 ∈ 𝐴 𝐵 ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) → 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 )
2	1	adantl	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ ( X 𝑘 ∈ 𝐴 𝐵 ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ) → 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 )
3		sseq1	⊢ ( ( 𝐵 ∖ 𝐶 ) = if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) → ( ( 𝐵 ∖ 𝐶 ) ⊆ 𝐵 ↔ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ⊆ 𝐵 ) )
4		sseq1	⊢ ( 𝐵 = if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) → ( 𝐵 ⊆ 𝐵 ↔ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ⊆ 𝐵 ) )
5		difss	⊢ ( 𝐵 ∖ 𝐶 ) ⊆ 𝐵
6		ssid	⊢ 𝐵 ⊆ 𝐵
7	3 4 5 6	keephyp	⊢ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ⊆ 𝐵
8	7	rgenw	⊢ ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ⊆ 𝐵
9		ss2ixp	⊢ ( ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ⊆ 𝐵 → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ⊆ X 𝑘 ∈ 𝐴 𝐵 )
10	8 9	mp1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) → X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ⊆ X 𝑘 ∈ 𝐴 𝐵 )
11	10	sselda	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ) → 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 )
12		vex	⊢ 𝑧 ∈ V
13	12	elixp	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) )
14		ixpfn	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 → 𝑧 Fn 𝐴 )
15	14	adantl	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → 𝑧 Fn 𝐴 )
16	15	biantrurd	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ) )
17	13 16	bitr4id	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) )
18	17	notbid	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ¬ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) )
19		rexnal	⊢ ( ∃ 𝑘 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) )
20		eleq2	⊢ ( ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) = if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) → ( ( 𝑧 ‘ 𝑚 ) ∈ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ↔ ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
21		eleq2	⊢ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) → ( ( 𝑧 ‘ 𝑚 ) ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ↔ ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
22		eleq2	⊢ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐶 = if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) → ( ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐶 ↔ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) )
23		eleq2	⊢ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) → ( ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ↔ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) )
24		simpl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) → 𝑋 ∈ 𝐴 )
25	12	elixp	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ 𝐵 ) )
26	25	simprbi	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 → ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ 𝐵 )
27		nfv	⊢ Ⅎ 𝑙 ( 𝑧 ‘ 𝑘 ) ∈ 𝐵
28		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐵
29	28	nfel2	⊢ Ⅎ 𝑘 ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵
30		fveq2	⊢ ( 𝑘 = 𝑙 → ( 𝑧 ‘ 𝑘 ) = ( 𝑧 ‘ 𝑙 ) )
31		csbeq1a	⊢ ( 𝑘 = 𝑙 → 𝐵 = ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
32	30 31	eleq12d	⊢ ( 𝑘 = 𝑙 → ( ( 𝑧 ‘ 𝑘 ) ∈ 𝐵 ↔ ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
33	27 29 32	cbvralw	⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ 𝐵 ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
34	26 33	sylib	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 → ∀ 𝑙 ∈ 𝐴 ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
35		fveq2	⊢ ( 𝑙 = 𝑋 → ( 𝑧 ‘ 𝑙 ) = ( 𝑧 ‘ 𝑋 ) )
36		csbeq1	⊢ ( 𝑙 = 𝑋 → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = ⦋ 𝑋 / 𝑘 ⦌ 𝐵 )
37	35 36	eleq12d	⊢ ( 𝑙 = 𝑋 → ( ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ↔ ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ) )
38	37	rspcva	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑙 ∈ 𝐴 ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) → ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐵 )
39	24 34 38	syl2an	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐵 )
40		neldif	⊢ ( ( ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) → ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 )
41	39 40	sylan	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) → ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 )
42	41	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) ∧ 𝑙 ∈ 𝐴 ) → ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 )
43		csbeq1	⊢ ( 𝑙 = 𝑋 → ⦋ 𝑙 / 𝑘 ⦌ 𝐶 = ⦋ 𝑋 / 𝑘 ⦌ 𝐶 )
44	35 43	eleq12d	⊢ ( 𝑙 = 𝑋 → ( ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐶 ↔ ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
45	42 44	syl5ibrcom	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) ∧ 𝑙 ∈ 𝐴 ) → ( 𝑙 = 𝑋 → ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐶 ) )
46	45	imp	⊢ ( ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) ∧ 𝑙 ∈ 𝐴 ) ∧ 𝑙 = 𝑋 ) → ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐶 )
47	34	ad2antlr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) → ∀ 𝑙 ∈ 𝐴 ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
48	47	r19.21bi	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) ∧ 𝑙 ∈ 𝐴 ) → ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
49	48	adantr	⊢ ( ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) ∧ 𝑙 ∈ 𝐴 ) ∧ ¬ 𝑙 = 𝑋 ) → ( 𝑧 ‘ 𝑙 ) ∈ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
50	22 23 46 49	ifbothda	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) ∧ 𝑙 ∈ 𝐴 ) → ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
51	50	ralrimiva	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) → ∀ 𝑙 ∈ 𝐴 ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
52		dfral2	⊢ ( ∀ 𝑙 ∈ 𝐴 ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ↔ ¬ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
53	51 52	sylib	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) → ¬ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
54	53	ex	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ¬ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) → ¬ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) )
55	54	con4d	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) → ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) )
56	55	imp	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) → ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
57	56	adantr	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
58		fveq2	⊢ ( 𝑚 = 𝑋 → ( 𝑧 ‘ 𝑚 ) = ( 𝑧 ‘ 𝑋 ) )
59		csbeq1	⊢ ( 𝑚 = 𝑋 → ⦋ 𝑚 / 𝑘 ⦌ 𝐵 = ⦋ 𝑋 / 𝑘 ⦌ 𝐵 )
60		csbeq1	⊢ ( 𝑚 = 𝑋 → ⦋ 𝑚 / 𝑘 ⦌ 𝐶 = ⦋ 𝑋 / 𝑘 ⦌ 𝐶 )
61	59 60	difeq12d	⊢ ( 𝑚 = 𝑋 → ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) = ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
62	58 61	eleq12d	⊢ ( 𝑚 = 𝑋 → ( ( 𝑧 ‘ 𝑚 ) ∈ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ↔ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) )
63	57 62	syl5ibrcom	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝑚 = 𝑋 → ( 𝑧 ‘ 𝑚 ) ∈ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) ) )
64	63	imp	⊢ ( ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) ∧ 𝑚 = 𝑋 ) → ( 𝑧 ‘ 𝑚 ) ∈ ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) )
65		nfv	⊢ Ⅎ 𝑚 ( 𝑧 ‘ 𝑘 ) ∈ 𝐵
66		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐵
67	66	nfel2	⊢ Ⅎ 𝑘 ( 𝑧 ‘ 𝑚 ) ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵
68		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝑧 ‘ 𝑘 ) = ( 𝑧 ‘ 𝑚 ) )
69		csbeq1a	⊢ ( 𝑘 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
70	68 69	eleq12d	⊢ ( 𝑘 = 𝑚 → ( ( 𝑧 ‘ 𝑘 ) ∈ 𝐵 ↔ ( 𝑧 ‘ 𝑚 ) ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
71	65 67 70	cbvralw	⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ 𝐵 ↔ ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
72	26 71	sylib	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 → ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
73	72	ad2antlr	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) → ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
74	73	r19.21bi	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝑧 ‘ 𝑚 ) ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
75	74	adantr	⊢ ( ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) ∧ ¬ 𝑚 = 𝑋 ) → ( 𝑧 ‘ 𝑚 ) ∈ ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
76	20 21 64 75	ifbothda	⊢ ( ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
77	76	ralrimiva	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) → ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
78		simpll	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → 𝑋 ∈ 𝐴 )
79		iftrue	⊢ ( 𝑚 = 𝑋 → if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) )
80	79 61	eqtrd	⊢ ( 𝑚 = 𝑋 → if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) = ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
81	58 80	eleq12d	⊢ ( 𝑚 = 𝑋 → ( ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) ) )
82	81	rspcva	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) → ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
83	78 82	sylan	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) → ( 𝑧 ‘ 𝑋 ) ∈ ( ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
84	83	eldifbd	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) → ¬ ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 )
85		iftrue	⊢ ( 𝑙 = 𝑋 → if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) = ⦋ 𝑙 / 𝑘 ⦌ 𝐶 )
86	85 43	eqtrd	⊢ ( 𝑙 = 𝑋 → if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) = ⦋ 𝑋 / 𝑘 ⦌ 𝐶 )
87	35 86	eleq12d	⊢ ( 𝑙 = 𝑋 → ( ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ↔ ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
88	87	notbid	⊢ ( 𝑙 = 𝑋 → ( ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ↔ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) )
89	88	rspcev	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ¬ ( 𝑧 ‘ 𝑋 ) ∈ ⦋ 𝑋 / 𝑘 ⦌ 𝐶 ) → ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
90	78 84 89	syl2an2r	⊢ ( ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) ∧ ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) → ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
91	77 90	impbida	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ↔ ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
92		nfv	⊢ Ⅎ 𝑙 ¬ ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 )
93		nfv	⊢ Ⅎ 𝑘 𝑙 = 𝑋
94		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐶
95	93 94 28	nfif	⊢ Ⅎ 𝑘 if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
96	95	nfel2	⊢ Ⅎ 𝑘 ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
97	96	nfn	⊢ Ⅎ 𝑘 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
98		eqeq1	⊢ ( 𝑘 = 𝑙 → ( 𝑘 = 𝑋 ↔ 𝑙 = 𝑋 ) )
99		csbeq1a	⊢ ( 𝑘 = 𝑙 → 𝐶 = ⦋ 𝑙 / 𝑘 ⦌ 𝐶 )
100	98 99 31	ifbieq12d	⊢ ( 𝑘 = 𝑙 → if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) = if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
101	30 100	eleq12d	⊢ ( 𝑘 = 𝑙 → ( ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) )
102	101	notbid	⊢ ( 𝑘 = 𝑙 → ( ¬ ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) ) )
103	92 97 102	cbvrexw	⊢ ( ∃ 𝑘 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∃ 𝑙 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑙 ) ∈ if ( 𝑙 = 𝑋 , ⦋ 𝑙 / 𝑘 ⦌ 𝐶 , ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) )
104		nfv	⊢ Ⅎ 𝑚 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 )
105		nfv	⊢ Ⅎ 𝑘 𝑚 = 𝑋
106		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐶
107	66 106	nfdif	⊢ Ⅎ 𝑘 ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
108	105 107 66	nfif	⊢ Ⅎ 𝑘 if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
109	108	nfel2	⊢ Ⅎ 𝑘 ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 )
110		eqeq1	⊢ ( 𝑘 = 𝑚 → ( 𝑘 = 𝑋 ↔ 𝑚 = 𝑋 ) )
111		csbeq1a	⊢ ( 𝑘 = 𝑚 → 𝐶 = ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
112	69 111	difeq12d	⊢ ( 𝑘 = 𝑚 → ( 𝐵 ∖ 𝐶 ) = ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) )
113	110 112 69	ifbieq12d	⊢ ( 𝑘 = 𝑚 → if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) = if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
114	68 113	eleq12d	⊢ ( 𝑘 = 𝑚 → ( ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ↔ ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) ) )
115	104 109 114	cbvralw	⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ↔ ∀ 𝑚 ∈ 𝐴 ( 𝑧 ‘ 𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ∖ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ) , ⦋ 𝑚 / 𝑘 ⦌ 𝐵 ) )
116	91 103 115	3bitr4g	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ∃ 𝑘 ∈ 𝐴 ¬ ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ) )
117	19 116	bitr3id	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ¬ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ) )
118	18 117	bitrd	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ¬ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ) )
119		ibar	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 → ( ¬ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ∧ ¬ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ) )
120	119	adantl	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ¬ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ∧ ¬ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ) )
121	15	biantrurd	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ) ) )
122	118 120 121	3bitr3d	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ∧ ¬ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ) ) )
123		eldif	⊢ ( 𝑧 ∈ ( X 𝑘 ∈ 𝐴 𝐵 ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ↔ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ∧ ¬ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) )
124	12	elixp	⊢ ( 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑧 ‘ 𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ) )
125	122 123 124	3bitr4g	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) ∧ 𝑧 ∈ X 𝑘 ∈ 𝐴 𝐵 ) → ( 𝑧 ∈ ( X 𝑘 ∈ 𝐴 𝐵 ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ↔ 𝑧 ∈ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) ) )
126	2 11 125	eqrdav	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ⊆ 𝐵 ) → ( X 𝑘 ∈ 𝐴 𝐵 ∖ X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) = X 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) )