Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  br8 Structured version   Unicode version
Theorem br8 30390
Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.)
Hypotheses
Ref Expression
br8.1 |- ( a = A -> ( ph <-> ps ) )
br8.2 |- ( b = B -> ( ps <-> ch ) )
br8.3 |- ( c = C -> ( ch <-> th ) )
br8.4 |- ( d = D -> ( th <-> ta ) )
br8.5 |- ( e = E -> ( ta <-> et ) )
br8.6 |- ( f = F -> ( et <-> ze ) )
br8.7 |- ( g = G -> ( ze <-> si ) )
br8.8 |- ( h = H -> ( si <-> rh ) )
br8.9 |- ( x = X -> P = Q )
br8.10 |- R = { <. p , q >. | E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) }
Assertion
Ref Expression
br8 |- ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> rh ) )
Distinct variable groups:   ch, b   et, e   a, b, c, d, e, f, g, h, p, q, P   ps, a   si, g   x, a, A, b, c, d, e, f, g, h, p, q   ph, p, q, x   rh, a, b, c, d, e, f, g, h, x   B, a, b, c, d, e, f, g, h, p, q, x   C, a, b, c, d, e, f, g, h, p, q, x   ta, d   D, a, b, c, d, e, f, g, h, p, q, x   E, a, b, c, d, e, f, g, h, p, q, x   th, c   F, a, b, c, d, e, f, g, h, p, q, x   G, a, b, c, d, e, f, g, h, p, q, x   ze, f   H, a, b, c, d, e, f, g, h, p, q, x   S, a, b, c, d, e, f, g, h, p, q, x   Q, a, b, c, d, e, f, g, h, x   X, a, b, c, d, e, f, g, h, x
Allowed substitution hints:   ph( e, f, g, h, a, b, c, d)   ps( x, e, f, g, h, q, p, b, c, d)   ch( x, e, f, g, h, q, p, a, c, d)   th( x, e, f, g, h, q, p, a, b, d)   ta( x, e, f, g, h, q, p, a, b, c)   et( x, f, g, h, q, p, a, b, c, d)   ze( x, e, g, h, q, p, a, b, c, d)   si( x, e, f, h, q, p, a, b, c, d)   rh( q, p)   P( x)   Q( q, p)   R( x, e, f, g, h, q, p, a, b, c, d)   X( q, p)
Proof of Theorem br8
StepHypRef Expression
1 opex 4681 . . 3 |- <. <. A , B >. , <. C , D >. >. e. _V
2 opex 4681 . . 3 |- <. <. E , F >. , <. G , H >. >. e. _V
3 eqeq1 2426 . . . . . . . . 9 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( p = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. ) )
433anbi1d 1339 . . . . . . . 8 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
54rexbidv 2939 . . . . . . 7 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
652rexbidv 2946 . . . . . 6 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
762rexbidv 2946 . . . . 5 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
872rexbidv 2946 . . . 4 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
982rexbidv 2946 . . 3 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
10 eqeq1 2426 . . . . . . . . 9 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( q = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) )
11103anbi2d 1340 . . . . . . . 8 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
1211rexbidv 2939 . . . . . . 7 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
13122rexbidv 2946 . . . . . 6 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
14132rexbidv 2946 . . . . 5 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
15142rexbidv 2946 . . . 4 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
16152rexbidv 2946 . . 3 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
17 br8.10 . . 3 |- R = { <. p , q >. | E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( p = <. <. a , b >. , <. c , d >. >. /\ q = <. <. e , f >. , <. g , h >. >. /\ ph ) }
181, 2, 9, 16, 17brab 4739 . 2 |- ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
19 opex 4681 . . . . . . . . . . . . . 14 |- <. a , b >. e. _V
20 opex 4681 . . . . . . . . . . . . . 14 |- <. c , d >. e. _V
2119, 20opth 4691 . . . . . . . . . . . . 13 |- ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. <-> ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) )
22 vex 3084 . . . . . . . . . . . . . . . 16 |- a e. _V
23 vex 3084 . . . . . . . . . . . . . . . 16 |- b e. _V
2422, 23opth 4691 . . . . . . . . . . . . . . 15 |- ( <. a , b >. = <. A , B >. <-> ( a = A /\ b = B ) )
25 br8.1 . . . . . . . . . . . . . . . 16 |- ( a = A -> ( ph <-> ps ) )
26 br8.2 . . . . . . . . . . . . . . . 16 |- ( b = B -> ( ps <-> ch ) )
2725, 26sylan9bb 704 . . . . . . . . . . . . . . 15 |- ( ( a = A /\ b = B ) -> ( ph <-> ch ) )
2824, 27sylbi 198 . . . . . . . . . . . . . 14 |- ( <. a , b >. = <. A , B >. -> ( ph <-> ch ) )
29 vex 3084 . . . . . . . . . . . . . . . 16 |- c e. _V
30 vex 3084 . . . . . . . . . . . . . . . 16 |- d e. _V
3129, 30opth 4691 . . . . . . . . . . . . . . 15 |- ( <. c , d >. = <. C , D >. <-> ( c = C /\ d = D ) )
32 br8.3 . . . . . . . . . . . . . . . 16 |- ( c = C -> ( ch <-> th ) )
33 br8.4 . . . . . . . . . . . . . . . 16 |- ( d = D -> ( th <-> ta ) )
3432, 33sylan9bb 704 . . . . . . . . . . . . . . 15 |- ( ( c = C /\ d = D ) -> ( ch <-> ta ) )
3531, 34sylbi 198 . . . . . . . . . . . . . 14 |- ( <. c , d >. = <. C , D >. -> ( ch <-> ta ) )
3628, 35sylan9bb 704 . . . . . . . . . . . . 13 |- ( ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) -> ( ph <-> ta ) )
3721, 36sylbi 198 . . . . . . . . . . . 12 |- ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. -> ( ph <-> ta ) )
3837eqcoms 2434 . . . . . . . . . . 11 |- ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. -> ( ph <-> ta ) )
39 opex 4681 . . . . . . . . . . . . . 14 |- <. e , f >. e. _V
40 opex 4681 . . . . . . . . . . . . . 14 |- <. g , h >. e. _V
4139, 40opth 4691 . . . . . . . . . . . . 13 |- ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. <-> ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) )
42 vex 3084 . . . . . . . . . . . . . . . 16 |- e e. _V
43 vex 3084 . . . . . . . . . . . . . . . 16 |- f e. _V
4442, 43opth 4691 . . . . . . . . . . . . . . 15 |- ( <. e , f >. = <. E , F >. <-> ( e = E /\ f = F ) )
45 br8.5 . . . . . . . . . . . . . . . 16 |- ( e = E -> ( ta <-> et ) )
46 br8.6 . . . . . . . . . . . . . . . 16 |- ( f = F -> ( et <-> ze ) )
4745, 46sylan9bb 704 . . . . . . . . . . . . . . 15 |- ( ( e = E /\ f = F ) -> ( ta <-> ze ) )
4844, 47sylbi 198 . . . . . . . . . . . . . 14 |- ( <. e , f >. = <. E , F >. -> ( ta <-> ze ) )
49 vex 3084 . . . . . . . . . . . . . . . 16 |- g e. _V
50 vex 3084 . . . . . . . . . . . . . . . 16 |- h e. _V
5149, 50opth 4691 . . . . . . . . . . . . . . 15 |- ( <. g , h >. = <. G , H >. <-> ( g = G /\ h = H ) )
52 br8.7 . . . . . . . . . . . . . . . 16 |- ( g = G -> ( ze <-> si ) )
53 br8.8 . . . . . . . . . . . . . . . 16 |- ( h = H -> ( si <-> rh ) )
5452, 53sylan9bb 704 . . . . . . . . . . . . . . 15 |- ( ( g = G /\ h = H ) -> ( ze <-> rh ) )
5551, 54sylbi 198 . . . . . . . . . . . . . 14 |- ( <. g , h >. = <. G , H >. -> ( ze <-> rh ) )
5648, 55sylan9bb 704 . . . . . . . . . . . . 13 |- ( ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) -> ( ta <-> rh ) )
5741, 56sylbi 198 . . . . . . . . . . . 12 |- ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. -> ( ta <-> rh ) )
5857eqcoms 2434 . . . . . . . . . . 11 |- ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. -> ( ta <-> rh ) )
5938, 58sylan9bb 704 . . . . . . . . . 10 |- ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) -> ( ph <-> rh ) )
6059biimp3a 1364 . . . . . . . . 9 |- ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh )
6160a1i 11 . . . . . . . 8 |- ( ( ( ( ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ ( x e. S /\ a e. P ) ) /\ ( b e. P /\ c e. P ) ) /\ ( d e. P /\ e e. P ) ) /\ ( f e. P /\ g e. P ) ) /\ h e. P ) -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
6261rexlimdva 2917 . . . . . . 7 |- ( ( ( ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ ( x e. S /\ a e. P ) ) /\ ( b e. P /\ c e. P ) ) /\ ( d e. P /\ e e. P ) ) /\ ( f e. P /\ g e. P ) ) -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
6362rexlimdvva 2924 . . . . . 6 |- ( ( ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ ( x e. S /\ a e. P ) ) /\ ( b e. P /\ c e. P ) ) /\ ( d e. P /\ e e. P ) ) -> ( E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
6463rexlimdvva 2924 . . . . 5 |- ( ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ ( x e. S /\ a e. P ) ) /\ ( b e. P /\ c e. P ) ) -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
6564rexlimdvva 2924 . . . 4 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ ( x e. S /\ a e. P ) ) -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
6665rexlimdvva 2924 . . 3 |- ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh ) )
67 simpl11 1080 . . . . 5 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> X e. S )
68 simpl12 1081 . . . . . 6 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> A e. Q )
69 simpl13 1082 . . . . . 6 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> B e. Q )
70 simpl21 1083 . . . . . 6 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> C e. Q )
71 simpl22 1084 . . . . . . 7 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> D e. Q )
72 simpl23 1085 . . . . . . 7 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E e. Q )
73 simpl31 1086 . . . . . . 7 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> F e. Q )
74 simpl32 1087 . . . . . . . 8 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> G e. Q )
75 simpl33 1088 . . . . . . . 8 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> H e. Q )
76 eqidd 2423 . . . . . . . 8 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. )
77 eqidd 2423 . . . . . . . 8 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. )
78 simpr 462 . . . . . . . 8 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> rh )
79 opeq1 4184 . . . . . . . . . . . 12 |- ( g = G -> <. g , h >. = <. G , h >. )
8079opeq2d 4191 . . . . . . . . . . 11 |- ( g = G -> <. <. E , F >. , <. g , h >. >. = <. <. E , F >. , <. G , h >. >. )
8180eqeq2d 2436 . . . . . . . . . 10 |- ( g = G -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. ) )
8281, 523anbi23d 1338 . . . . . . . . 9 |- ( g = G -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. /\ si ) ) )
83 opeq2 4185 . . . . . . . . . . . 12 |- ( h = H -> <. G , h >. = <. G , H >. )
8483opeq2d 4191 . . . . . . . . . . 11 |- ( h = H -> <. <. E , F >. , <. G , h >. >. = <. <. E , F >. , <. G , H >. >. )
8584eqeq2d 2436 . . . . . . . . . 10 |- ( h = H -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. ) )
8685, 533anbi23d 1338 . . . . . . . . 9 |- ( h = H -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. /\ si ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. /\ rh ) ) )
8782, 86rspc2ev 3193 . . . . . . . 8 |- ( ( G e. Q /\ H e. Q /\ ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. /\ rh ) ) -> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) )
8874, 75, 76, 77, 78, 87syl113anc 1276 . . . . . . 7 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) )
89 opeq2 4185 . . . . . . . . . . . 12 |- ( d = D -> <. C , d >. = <. C , D >. )
9089opeq2d 4191 . . . . . . . . . . 11 |- ( d = D -> <. <. A , B >. , <. C , d >. >. = <. <. A , B >. , <. C , D >. >. )
9190eqeq2d 2436 . . . . . . . . . 10 |- ( d = D -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. ) )
9291, 333anbi13d 1337 . . . . . . . . 9 |- ( d = D -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) ) )
93922rexbidv 2946 . . . . . . . 8 |- ( d = D -> ( E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) <-> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) ) )
94 opeq1 4184 . . . . . . . . . . . 12 |- ( e = E -> <. e , f >. = <. E , f >. )
9594opeq1d 4190 . . . . . . . . . . 11 |- ( e = E -> <. <. e , f >. , <. g , h >. >. = <. <. E , f >. , <. g , h >. >. )
9695eqeq2d 2436 . . . . . . . . . 10 |- ( e = E -> ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. ) )
9796, 453anbi23d 1338 . . . . . . . . 9 |- ( e = E -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ et ) ) )
98972rexbidv 2946 . . . . . . . 8 |- ( e = E -> ( E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ta ) <-> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ et ) ) )
99 opeq2 4185 . . . . . . . . . . . 12 |- ( f = F -> <. E , f >. = <. E , F >. )
10099opeq1d 4190 . . . . . . . . . . 11 |- ( f = F -> <. <. E , f >. , <. g , h >. >. = <. <. E , F >. , <. g , h >. >. )
101100eqeq2d 2436 . . . . . . . . . 10 |- ( f = F -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. ) )
102101, 463anbi23d 1338 . . . . . . . . 9 |- ( f = F -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ et ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) ) )
1031022rexbidv 2946 . . . . . . . 8 |- ( f = F -> ( E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. /\ et ) <-> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) ) )
10493, 98, 103rspc3ev 3195 . . . . . . 7 |- ( ( ( D e. Q /\ E e. Q /\ F e. Q ) /\ E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. /\ ze ) ) -> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) )
10571, 72, 73, 88, 104syl31anc 1267 . . . . . 6 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) )
106 opeq1 4184 . . . . . . . . . . . . 13 |- ( a = A -> <. a , b >. = <. A , b >. )
107106opeq1d 4190 . . . . . . . . . . . 12 |- ( a = A -> <. <. a , b >. , <. c , d >. >. = <. <. A , b >. , <. c , d >. >. )
108107eqeq2d 2436 . . . . . . . . . . 11 |- ( a = A -> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. ) )
109108, 253anbi13d 1337 . . . . . . . . . 10 |- ( a = A -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
110109rexbidv 2939 . . . . . . . . 9 |- ( a = A -> ( E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
1111102rexbidv 2946 . . . . . . . 8 |- ( a = A -> ( E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
1121112rexbidv 2946 . . . . . . 7 |- ( a = A -> ( E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) ) )
113 opeq2 4185 . . . . . . . . . . . . 13 |- ( b = B -> <. A , b >. = <. A , B >. )
114113opeq1d 4190 . . . . . . . . . . . 12 |- ( b = B -> <. <. A , b >. , <. c , d >. >. = <. <. A , B >. , <. c , d >. >. )
115114eqeq2d 2436 . . . . . . . . . . 11 |- ( b = B -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. ) )
116115, 263anbi13d 1337 . . . . . . . . . 10 |- ( b = B -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
117116rexbidv 2939 . . . . . . . . 9 |- ( b = B -> ( E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
1181172rexbidv 2946 . . . . . . . 8 |- ( b = B -> ( E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
1191182rexbidv 2946 . . . . . . 7 |- ( b = B -> ( E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ps ) <-> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) ) )
120 opeq1 4184 . . . . . . . . . . . . 13 |- ( c = C -> <. c , d >. = <. C , d >. )
121120opeq2d 4191 . . . . . . . . . . . 12 |- ( c = C -> <. <. A , B >. , <. c , d >. >. = <. <. A , B >. , <. C , d >. >. )
122121eqeq2d 2436 . . . . . . . . . . 11 |- ( c = C -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. ) )
123122, 323anbi13d 1337 . . . . . . . . . 10 |- ( c = C -> ( ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
124123rexbidv 2939 . . . . . . . . 9 |- ( c = C -> ( E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
1251242rexbidv 2946 . . . . . . . 8 |- ( c = C -> ( E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
1261252rexbidv 2946 . . . . . . 7 |- ( c = C -> ( E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ch ) <-> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) )
127112, 119, 126rspc3ev 3195 . . . . . 6 |- ( ( ( A e. Q /\ B e. Q /\ C e. Q ) /\ E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ th ) ) -> E. a e. Q E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
12868, 69, 70, 105, 127syl31anc 1267 . . . . 5 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E. a e. Q E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
129 br8.9 . . . . . . 7 |- ( x = X -> P = Q )
130129rexeqdv 3032 . . . . . . . . . . . . 13 |- ( x = X -> ( E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
131129, 130rexeqbidv 3040 . . . . . . . . . . . 12 |- ( x = X -> ( E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
132129, 131rexeqbidv 3040 . . . . . . . . . . 11 |- ( x = X -> ( E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
133129, 132rexeqbidv 3040 . . . . . . . . . 10 |- ( x = X -> ( E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
134129, 133rexeqbidv 3040 . . . . . . . . 9 |- ( x = X -> ( E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
135129, 134rexeqbidv 3040 . . . . . . . 8 |- ( x = X -> ( E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
136129, 135rexeqbidv 3040 . . . . . . 7 |- ( x = X -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
137129, 136rexeqbidv 3040 . . . . . 6 |- ( x = X -> ( E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> E. a e. Q E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
138137rspcev 3182 . . . . 5 |- ( ( X e. S /\ E. a e. Q E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q E. g e. Q E. h e. Q ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) -> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
13967, 128, 138syl2anc 665 . . . 4 |- ( ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) /\ rh ) -> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) )
140139ex 435 . . 3 |- ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( rh -> E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) ) )
14166, 140impbid 193 . 2 |- ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( E. x e. S E. a e. P E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P E. g e. P E. h e. P ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) <-> rh ) )
14218, 141syl5bb 260 1 |- ( ( ( X e. S /\ A e. Q /\ B e. Q ) /\ ( C e. Q /\ D e. Q /\ E e. Q ) /\ ( F e. Q /\ G e. Q /\ H e. Q ) ) -> ( <. <. A , B >. , <. C , D >. >. R <. <. E , F >. , <. G , H >. >. <-> rh ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1868   E.wrex 2776   <.cop 4002   class class class wbr 4420   {copab 4478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480
This theorem is referenced by:  brofs  30764  brifs  30802  brfs  30838
  Copyright terms: Public domain W3C validator