Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  br8 Structured version   Unicode version
Theorem br8 29360
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 4720 . . 3 |- <. <. A , B >. , <. C , D >. >. e. _V
2 opex 4720 . . 3 |- <. <. E , F >. , <. G , H >. >. e. _V
3 eqeq1 2461 . . . . . . . . 9 |- ( p = <. <. A , B >. , <. C , D >. >. -> ( p = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. ) )
433anbi1d 1303 . . . . . . . 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 2968 . . . . . . 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 2975 . . . . . 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 2975 . . . . 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 2975 . . . 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 2975 . . 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 2461 . . . . . . . . 9 |- ( q = <. <. E , F >. , <. G , H >. >. -> ( q = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) )
11103anbi2d 1304 . . . . . . . 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 2968 . . . . . . 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 2975 . . . . . 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 2975 . . . . 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 2975 . . . 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 2975 . . 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 4779 . 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 4720 . . . . . . . . . . . . . 14 |- <. a , b >. e. _V
20 opex 4720 . . . . . . . . . . . . . 14 |- <. c , d >. e. _V
2119, 20opth 4730 . . . . . . . . . . . . 13 |- ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. <-> ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) )
22 vex 3112 . . . . . . . . . . . . . . . 16 |- a e. _V
23 vex 3112 . . . . . . . . . . . . . . . 16 |- b e. _V
2422, 23opth 4730 . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . 15 |- ( ( a = A /\ b = B ) -> ( ph <-> ch ) )
2824, 27sylbi 195 . . . . . . . . . . . . . 14 |- ( <. a , b >. = <. A , B >. -> ( ph <-> ch ) )
29 vex 3112 . . . . . . . . . . . . . . . 16 |- c e. _V
30 vex 3112 . . . . . . . . . . . . . . . 16 |- d e. _V
3129, 30opth 4730 . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . 15 |- ( ( c = C /\ d = D ) -> ( ch <-> ta ) )
3531, 34sylbi 195 . . . . . . . . . . . . . 14 |- ( <. c , d >. = <. C , D >. -> ( ch <-> ta ) )
3628, 35sylan9bb 699 . . . . . . . . . . . . 13 |- ( ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) -> ( ph <-> ta ) )
3721, 36sylbi 195 . . . . . . . . . . . 12 |- ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. -> ( ph <-> ta ) )
3837eqcoms 2469 . . . . . . . . . . 11 |- ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. -> ( ph <-> ta ) )
39 opex 4720 . . . . . . . . . . . . . 14 |- <. e , f >. e. _V
40 opex 4720 . . . . . . . . . . . . . 14 |- <. g , h >. e. _V
4139, 40opth 4730 . . . . . . . . . . . . 13 |- ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. <-> ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) )
42 vex 3112 . . . . . . . . . . . . . . . 16 |- e e. _V
43 vex 3112 . . . . . . . . . . . . . . . 16 |- f e. _V
4442, 43opth 4730 . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . 15 |- ( ( e = E /\ f = F ) -> ( ta <-> ze ) )
4844, 47sylbi 195 . . . . . . . . . . . . . 14 |- ( <. e , f >. = <. E , F >. -> ( ta <-> ze ) )
49 vex 3112 . . . . . . . . . . . . . . . 16 |- g e. _V
50 vex 3112 . . . . . . . . . . . . . . . 16 |- h e. _V
5149, 50opth 4730 . . . . . . . . . . . . . . 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 699 . . . . . . . . . . . . . . 15 |- ( ( g = G /\ h = H ) -> ( ze <-> rh ) )
5551, 54sylbi 195 . . . . . . . . . . . . . 14 |- ( <. g , h >. = <. G , H >. -> ( ze <-> rh ) )
5648, 55sylan9bb 699 . . . . . . . . . . . . 13 |- ( ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) -> ( ta <-> rh ) )
5741, 56sylbi 195 . . . . . . . . . . . 12 |- ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. -> ( ta <-> rh ) )
5857eqcoms 2469 . . . . . . . . . . 11 |- ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. -> ( ta <-> rh ) )
5938, 58sylan9bb 699 . . . . . . . . . 10 |- ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) -> ( ph <-> rh ) )
6059biimp3a 1328 . . . . . . . . 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 2949 . . . . . . 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 2956 . . . . . 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 2956 . . . . 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 2956 . . . 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 2956 . . 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 1071 . . . . 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 1072 . . . . . 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 1073 . . . . . 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 1074 . . . . . 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 1075 . . . . . . 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 1076 . . . . . . 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 1077 . . . . . . 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 1078 . . . . . . . 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 1079 . . . . . . . 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 2458 . . . . . . . 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 2458 . . . . . . . 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 461 . . . . . . . 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 4219 . . . . . . . . . . . 12 |- ( g = G -> <. g , h >. = <. G , h >. )
8079opeq2d 4226 . . . . . . . . . . 11 |- ( g = G -> <. <. E , F >. , <. g , h >. >. = <. <. E , F >. , <. G , h >. >. )
8180eqeq2d 2471 . . . . . . . . . 10 |- ( g = G -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. ) )
8281, 523anbi23d 1302 . . . . . . . . 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 4220 . . . . . . . . . . . 12 |- ( h = H -> <. G , h >. = <. G , H >. )
8483opeq2d 4226 . . . . . . . . . . 11 |- ( h = H -> <. <. E , F >. , <. G , h >. >. = <. <. E , F >. , <. G , H >. >. )
8584eqeq2d 2471 . . . . . . . . . 10 |- ( h = H -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. ) )
8685, 533anbi23d 1302 . . . . . . . . 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 3221 . . . . . . . 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 1240 . . . . . . 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 4220 . . . . . . . . . . . 12 |- ( d = D -> <. C , d >. = <. C , D >. )
9089opeq2d 4226 . . . . . . . . . . 11 |- ( d = D -> <. <. A , B >. , <. C , d >. >. = <. <. A , B >. , <. C , D >. >. )
9190eqeq2d 2471 . . . . . . . . . 10 |- ( d = D -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. ) )
9291, 333anbi13d 1301 . . . . . . . . 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 2975 . . . . . . . 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 4219 . . . . . . . . . . . 12 |- ( e = E -> <. e , f >. = <. E , f >. )
9594opeq1d 4225 . . . . . . . . . . 11 |- ( e = E -> <. <. e , f >. , <. g , h >. >. = <. <. E , f >. , <. g , h >. >. )
9695eqeq2d 2471 . . . . . . . . . 10 |- ( e = E -> ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. ) )
9796, 453anbi23d 1302 . . . . . . . . 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 2975 . . . . . . . 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 4220 . . . . . . . . . . . 12 |- ( f = F -> <. E , f >. = <. E , F >. )
10099opeq1d 4225 . . . . . . . . . . 11 |- ( f = F -> <. <. E , f >. , <. g , h >. >. = <. <. E , F >. , <. g , h >. >. )
101100eqeq2d 2471 . . . . . . . . . 10 |- ( f = F -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. ) )
102101, 463anbi23d 1302 . . . . . . . . 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 2975 . . . . . . . 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 3223 . . . . . . 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 1231 . . . . . 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 4219 . . . . . . . . . . . . 13 |- ( a = A -> <. a , b >. = <. A , b >. )
107106opeq1d 4225 . . . . . . . . . . . 12 |- ( a = A -> <. <. a , b >. , <. c , d >. >. = <. <. A , b >. , <. c , d >. >. )
108107eqeq2d 2471 . . . . . . . . . . 11 |- ( a = A -> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. ) )
109108, 253anbi13d 1301 . . . . . . . . . 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 2968 . . . . . . . . 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 2975 . . . . . . . 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 2975 . . . . . . 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 4220 . . . . . . . . . . . . 13 |- ( b = B -> <. A , b >. = <. A , B >. )
114113opeq1d 4225 . . . . . . . . . . . 12 |- ( b = B -> <. <. A , b >. , <. c , d >. >. = <. <. A , B >. , <. c , d >. >. )
115114eqeq2d 2471 . . . . . . . . . . 11 |- ( b = B -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. ) )
116115, 263anbi13d 1301 . . . . . . . . . 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 2968 . . . . . . . . 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 2975 . . . . . . . 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 2975 . . . . . . 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 4219 . . . . . . . . . . . . 13 |- ( c = C -> <. c , d >. = <. C , d >. )
121120opeq2d 4226 . . . . . . . . . . . 12 |- ( c = C -> <. <. A , B >. , <. c , d >. >. = <. <. A , B >. , <. C , d >. >. )
122121eqeq2d 2471 . . . . . . . . . . 11 |- ( c = C -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. ) )
123122, 323anbi13d 1301 . . . . . . . . . 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 2968 . . . . . . . . 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 2975 . . . . . . . 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 2975 . . . . . . 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 3223 . . . . . 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 1231 . . . . 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 3061 . . . . . . . . . . . . 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 3069 . . . . . . . . . . . 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 3069 . . . . . . . . . . 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 3069 . . . . . . . . . 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 3069 . . . . . . . . 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 3069 . . . . . . . 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 3069 . . . . . . 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 3069 . . . . . 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 3210 . . . . 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 661 . . . 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 434 . . 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 191 . 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 257 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 184   /\ wa 369   /\ w3a 973   = wceq 1395   e. wcel 1819   E.wrex 2808   <.cop 4038   class class class wbr 4456   {copab 4514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516
This theorem is referenced by:  brofs  29817  brifs  29855  brfs  29891
  Copyright terms: Public domain W3C validator