This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑘 = 𝑋 , ( 𝐵 ∖ 𝐶 ) , 𝐵 ) )