Metamath Proof Explorer

Theorem relpropg

Description: A pair of ordered pairs is a relation. (Contributed by Eric Schmidt, 24-Oct-2026)

Ref Expression
Assertion relpropg 
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> Rel { <. A , B >. , <. C , D >. } )

Proof

Step Hyp Ref Expression
1 relsnopg 
 |-  ( ( A e. V /\ B e. W ) -> Rel { <. A , B >. } )
2 relsnopg 
 |-  ( ( C e. X /\ D e. Y ) -> Rel { <. C , D >. } )
3 1 2 anim12i 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( Rel { <. A , B >. } /\ Rel { <. C , D >. } ) )
4 relun 
 |-  ( Rel ( { <. A , B >. } u. { <. C , D >. } ) <-> ( Rel { <. A , B >. } /\ Rel { <. C , D >. } ) )
5 3 4 sylibr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> Rel ( { <. A , B >. } u. { <. C , D >. } ) )
6 df-pr 
 |-  { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } )
7 6 releqi 
 |-  ( Rel { <. A , B >. , <. C , D >. } <-> Rel ( { <. A , B >. } u. { <. C , D >. } ) )
8 5 7 sylibr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> Rel { <. A , B >. , <. C , D >. } )