Step 
Hyp 
Ref 
Expression 
1 

elxp 
⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑏 ∃ 𝑐 ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ) 
2 

vex 
⊢ 𝑏 ∈ V 
3 

vex 
⊢ 𝑐 ∈ V 
4 
2 3

op1std 
⊢ ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ → ( 1^{st} ‘ 𝐴 ) = 𝑏 ) 
5 
4

eleq1d 
⊢ ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ → ( ( 1^{st} ‘ 𝐴 ) ∈ 𝐵 ↔ 𝑏 ∈ 𝐵 ) ) 
6 
5

biimpar 
⊢ ( ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ 𝑏 ∈ 𝐵 ) → ( 1^{st} ‘ 𝐴 ) ∈ 𝐵 ) 
7 
6

adantrr 
⊢ ( ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 1^{st} ‘ 𝐴 ) ∈ 𝐵 ) 
8 
7

exlimivv 
⊢ ( ∃ 𝑏 ∃ 𝑐 ( 𝐴 = ⟨ 𝑏 , 𝑐 ⟩ ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( 1^{st} ‘ 𝐴 ) ∈ 𝐵 ) 
9 
1 8

sylbi 
⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → ( 1^{st} ‘ 𝐴 ) ∈ 𝐵 ) 