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

Metamath Proof Explorer

Theorem 2rbropap

Description: Properties of a pair in a restricted binary relation M expressed as an ordered-pair class abstraction: M is the binary relation W restricted by the conditions ps and ta . (Contributed by AV, 31-Jan-2021)

Ref Expression
Hypotheses 2rbropap.1 
|- ( ph -> M = { <. f , p >. | ( f W p /\ ps /\ ta ) } )
2rbropap.2 
|- ( ( f = F /\ p = P ) -> ( ps <-> ch ) )
2rbropap.3 
|- ( ( f = F /\ p = P ) -> ( ta <-> th ) )
Assertion 2rbropap 
|- ( ( ph /\ F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch /\ th ) ) )

Proof

Step Hyp Ref Expression
1 2rbropap.1 
 |-  ( ph -> M = { <. f , p >. | ( f W p /\ ps /\ ta ) } )
2 2rbropap.2 
 |-  ( ( f = F /\ p = P ) -> ( ps <-> ch ) )
3 2rbropap.3 
 |-  ( ( f = F /\ p = P ) -> ( ta <-> th ) )
4 3anass 
 |-  ( ( f W p /\ ps /\ ta ) <-> ( f W p /\ ( ps /\ ta ) ) )
5 4 opabbii 
 |-  { <. f , p >. | ( f W p /\ ps /\ ta ) } = { <. f , p >. | ( f W p /\ ( ps /\ ta ) ) }
6 1 5 eqtrdi 
 |-  ( ph -> M = { <. f , p >. | ( f W p /\ ( ps /\ ta ) ) } )
7 2 3 anbi12d 
 |-  ( ( f = F /\ p = P ) -> ( ( ps /\ ta ) <-> ( ch /\ th ) ) )
8 6 7 rbropap 
 |-  ( ( ph /\ F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ( ch /\ th ) ) ) )
9 3anass 
 |-  ( ( F W P /\ ch /\ th ) <-> ( F W P /\ ( ch /\ th ) ) )
10 8 9 bitr4di 
 |-  ( ( ph /\ F e. X /\ P e. Y ) -> ( F M P <-> ( F W P /\ ch /\ th ) ) )