Metamath Proof Explorer

Theorem elrelb

Description: A member of a relation expressed by an ordered pair. (Contributed by AV, 23-Aug-2026)

Ref Expression
Assertion elrelb 
|- ( Rel R -> ( A e. R <-> E. x E. y ( A = <. x , y >. /\ x R y ) ) )

Proof

Step Hyp Ref Expression
1 elrel 
 |-  ( ( Rel R /\ A e. R ) -> E. x E. y A = <. x , y >. )
2 eleq1 
 |-  ( A = <. x , y >. -> ( A e. R <-> <. x , y >. e. R ) )
3 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
4 3 biimpri 
 |-  ( <. x , y >. e. R -> x R y )
5 2 4 biimtrdi 
 |-  ( A = <. x , y >. -> ( A e. R -> x R y ) )
6 5 com12 
 |-  ( A e. R -> ( A = <. x , y >. -> x R y ) )
7 6 adantl 
 |-  ( ( Rel R /\ A e. R ) -> ( A = <. x , y >. -> x R y ) )
8 7 ancld 
 |-  ( ( Rel R /\ A e. R ) -> ( A = <. x , y >. -> ( A = <. x , y >. /\ x R y ) ) )
9 8 2eximdv 
 |-  ( ( Rel R /\ A e. R ) -> ( E. x E. y A = <. x , y >. -> E. x E. y ( A = <. x , y >. /\ x R y ) ) )
10 1 9 mpd 
 |-  ( ( Rel R /\ A e. R ) -> E. x E. y ( A = <. x , y >. /\ x R y ) )
11 10 ex 
 |-  ( Rel R -> ( A e. R -> E. x E. y ( A = <. x , y >. /\ x R y ) ) )
12 3 bilani 
 |-  ( ( A = <. x , y >. /\ x R y ) -> <. x , y >. e. R )
13 2 adantr 
 |-  ( ( A = <. x , y >. /\ x R y ) -> ( A e. R <-> <. x , y >. e. R ) )
14 12 13 mpbird 
 |-  ( ( A = <. x , y >. /\ x R y ) -> A e. R )
15 14 exlimiv 
 |-  ( E. y ( A = <. x , y >. /\ x R y ) -> A e. R )
16 15 exlimiv 
 |-  ( E. x E. y ( A = <. x , y >. /\ x R y ) -> A e. R )
17 11 16 impbid1 
 |-  ( Rel R -> ( A e. R <-> E. x E. y ( A = <. x , y >. /\ x R y ) ) )