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 V
Assertion brtxp2 A R S B x y B = x y A R x A S y

Proof

Step Hyp Ref Expression
1 brtxp2.1 A V
2 txpss3v R S V × V × V
3 2 brel A R S B A V B V × V
4 3 simprd A R S B B V × V
5 elvv B V × V x y B = x y
6 4 5 sylib A R S B x y B = x y
7 6 pm4.71ri A R S B x y B = x y A R S B
8 19.41vv x y B = x y A R S B x y B = x y A R S B
9 7 8 bitr4i A R S B x y B = x y A R S B
10 breq2 B = x y A R S B A R S x y
11 10 pm5.32i B = x y A R S B B = x y A R S x y
12 11 2exbii x y B = x y A R S B x y B = x y A R S x y
13 vex x V
14 vex y V
15 1 13 14 brtxp A R S x y A R x A S y
16 15 anbi2i B = x y A R 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 S x y B = x y A R x A S y
19 18 2exbii x y B = x y A R S x y x y B = x y A R x A S y
20 9 12 19 3bitri A R S B x y B = x y A R x A S y