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 ) )