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

Metamath Proof Explorer

Theorem xrneq12d

Description: Equality theorem for the range Cartesian product, deduction form. (Contributed by Peter Mazsa, 18-Dec-2021)

Ref Expression
Hypotheses xrneq12d.1 
|- ( ph -> A = B )
xrneq12d.2 
|- ( ph -> C = D )
Assertion xrneq12d 
|- ( ph -> ( A |X. C ) = ( B |X. D ) )

Proof

Step Hyp Ref Expression
1 xrneq12d.1 
 |-  ( ph -> A = B )
2 xrneq12d.2 
 |-  ( ph -> C = D )
3 xrneq12 
 |-  ( ( A = B /\ C = D ) -> ( A |X. C ) = ( B |X. D ) )
4 1 2 3 syl2anc 
 |-  ( ph -> ( A |X. C ) = ( B |X. D ) )