Step 
Hyp 
Ref 
Expression 
1 

f1imass 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ↔ 𝐶 ⊆ 𝐷 ) ) 
2 

f1imass 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ( 𝐷 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐷 ) ⊆ ( 𝐹 “ 𝐶 ) ↔ 𝐷 ⊆ 𝐶 ) ) 
3 
2

ancom2s 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐷 ) ⊆ ( 𝐹 “ 𝐶 ) ↔ 𝐷 ⊆ 𝐶 ) ) 
4 
1 3

anbi12d 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ∧ ( 𝐹 “ 𝐷 ) ⊆ ( 𝐹 “ 𝐶 ) ) ↔ ( 𝐶 ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐶 ) ) ) 
5 

eqss 
⊢ ( ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ↔ ( ( 𝐹 “ 𝐶 ) ⊆ ( 𝐹 “ 𝐷 ) ∧ ( 𝐹 “ 𝐷 ) ⊆ ( 𝐹 “ 𝐶 ) ) ) 
6 

eqss 
⊢ ( 𝐶 = 𝐷 ↔ ( 𝐶 ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐶 ) ) 
7 
4 5 6

3bitr4g 
⊢ ( ( 𝐹 : 𝐴 –11→ 𝐵 ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐴 ) ) → ( ( 𝐹 “ 𝐶 ) = ( 𝐹 “ 𝐷 ) ↔ 𝐶 = 𝐷 ) ) 