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

Metamath Proof Explorer

Theorem brtxp2

Description: The binary relation over a tail cross when the second argument is not an ordered pair. (Contributed by Scott Fenton, 14-Apr-2014) (Revised by Mario Carneiro, 3-May-2015)

Ref Expression
Hypothesis brtxp2.1 
|- A e. _V
Assertion brtxp2 
|- ( A ( R (x) S ) B <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) )

Proof

Step Hyp Ref Expression
1 brtxp2.1 
 |-  A e. _V
2 txpss3v 
 |-  ( R (x) S ) C_ ( _V X. ( _V X. _V ) )
3 2 brel 
 |-  ( A ( R (x) S ) B -> ( A e. _V /\ B e. ( _V X. _V ) ) )
4 3 simprd 
 |-  ( A ( R (x) S ) B -> B e. ( _V X. _V ) )
5 elvv 
 |-  ( B e. ( _V X. _V ) <-> E. x E. y B = <. x , y >. )
6 4 5 sylib 
 |-  ( A ( R (x) S ) B -> E. x E. y B = <. x , y >. )
7 6 pm4.71ri 
 |-  ( A ( R (x) S ) B <-> ( E. x E. y B = <. x , y >. /\ A ( R (x) S ) B ) )
8 19.41vv 
 |-  ( E. x E. y ( B = <. x , y >. /\ A ( R (x) S ) B ) <-> ( E. x E. y B = <. x , y >. /\ A ( R (x) S ) B ) )
9 7 8 bitr4i 
 |-  ( A ( R (x) S ) B <-> E. x E. y ( B = <. x , y >. /\ A ( R (x) S ) B ) )
10 breq2 
 |-  ( B = <. x , y >. -> ( A ( R (x) S ) B <-> A ( R (x) S ) <. x , y >. ) )
11 10 pm5.32i 
 |-  ( ( B = <. x , y >. /\ A ( R (x) S ) B ) <-> ( B = <. x , y >. /\ A ( R (x) S ) <. x , y >. ) )
12 11 2exbii 
 |-  ( E. x E. y ( B = <. x , y >. /\ A ( R (x) S ) B ) <-> E. x E. y ( B = <. x , y >. /\ A ( R (x) S ) <. x , y >. ) )
13 vex 
 |-  x e. _V
14 vex 
 |-  y e. _V
15 1 13 14 brtxp 
 |-  ( A ( R (x) S ) <. x , y >. <-> ( A R x /\ A S y ) )
16 15 anbi2i 
 |-  ( ( B = <. x , y >. /\ A ( R (x) S ) <. x , y >. ) <-> ( B = <. x , y >. /\ ( A R x /\ A S y ) ) )
17 3anass 
 |-  ( ( B = <. x , y >. /\ A R x /\ A S y ) <-> ( B = <. x , y >. /\ ( A R x /\ A S y ) ) )
18 16 17 bitr4i 
 |-  ( ( B = <. x , y >. /\ A ( R (x) S ) <. x , y >. ) <-> ( B = <. x , y >. /\ A R x /\ A S y ) )
19 18 2exbii 
 |-  ( E. x E. y ( B = <. x , y >. /\ A ( R (x) S ) <. x , y >. ) <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) )
20 9 12 19 3bitri 
 |-  ( A ( R (x) S ) B <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) )