br8

Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013) (Revised by Mario Carneiro, 3-May-2015)

	Ref	Expression
Hypotheses	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	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 ) )

Proof

Step	Hyp	Ref	Expression
1		br8.1	\|- ( a = A -> ( ph <-> ps ) )
2		br8.2	\|- ( b = B -> ( ps <-> ch ) )
3		br8.3	\|- ( c = C -> ( ch <-> th ) )
4		br8.4	\|- ( d = D -> ( th <-> ta ) )
5		br8.5	\|- ( e = E -> ( ta <-> et ) )
6		br8.6	\|- ( f = F -> ( et <-> ze ) )
7		br8.7	\|- ( g = G -> ( ze <-> si ) )
8		br8.8	\|- ( h = H -> ( si <-> rh ) )
9		br8.9	\|- ( x = X -> P = Q )
10		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 ) }
11		opex	\|- <. <. A , B >. , <. C , D >. >. e. _V
12		opex	\|- <. <. E , F >. , <. G , H >. >. e. _V
13		eqeq1	\|- ( p = <. <. A , B >. , <. C , D >. >. -> ( p = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. ) )
14	13	3anbi1d	\|- ( 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 ) ) )
15	14	rexbidv	\|- ( 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 ) ) )
16	15	2rexbidv	\|- ( 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 ) ) )
17	16	2rexbidv	\|- ( 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 ) ) )
18	17	2rexbidv	\|- ( 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 ) ) )
19	18	2rexbidv	\|- ( 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 ) ) )
20		eqeq1	\|- ( q = <. <. E , F >. , <. G , H >. >. -> ( q = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) )
21	20	3anbi2d	\|- ( 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 ) ) )
22	21	rexbidv	\|- ( 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 ) ) )
23	22	2rexbidv	\|- ( 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 ) ) )
24	23	2rexbidv	\|- ( 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 ) ) )
25	24	2rexbidv	\|- ( 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 ) ) )
26	25	2rexbidv	\|- ( 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 ) ) )
27	11 12 19 26 10	brab	\|- ( <. <. 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 ) )
28		opex	\|- <. a , b >. e. _V
29		opex	\|- <. c , d >. e. _V
30	28 29	opth	\|- ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. <-> ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) )
31		vex	\|- a e. _V
32		vex	\|- b e. _V
33	31 32	opth	\|- ( <. a , b >. = <. A , B >. <-> ( a = A /\ b = B ) )
34	1 2	sylan9bb	\|- ( ( a = A /\ b = B ) -> ( ph <-> ch ) )
35	33 34	sylbi	\|- ( <. a , b >. = <. A , B >. -> ( ph <-> ch ) )
36		vex	\|- c e. _V
37		vex	\|- d e. _V
38	36 37	opth	\|- ( <. c , d >. = <. C , D >. <-> ( c = C /\ d = D ) )
39	3 4	sylan9bb	\|- ( ( c = C /\ d = D ) -> ( ch <-> ta ) )
40	38 39	sylbi	\|- ( <. c , d >. = <. C , D >. -> ( ch <-> ta ) )
41	35 40	sylan9bb	\|- ( ( <. a , b >. = <. A , B >. /\ <. c , d >. = <. C , D >. ) -> ( ph <-> ta ) )
42	30 41	sylbi	\|- ( <. <. a , b >. , <. c , d >. >. = <. <. A , B >. , <. C , D >. >. -> ( ph <-> ta ) )
43	42	eqcoms	\|- ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. -> ( ph <-> ta ) )
44		opex	\|- <. e , f >. e. _V
45		opex	\|- <. g , h >. e. _V
46	44 45	opth	\|- ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. <-> ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) )
47		vex	\|- e e. _V
48		vex	\|- f e. _V
49	47 48	opth	\|- ( <. e , f >. = <. E , F >. <-> ( e = E /\ f = F ) )
50	5 6	sylan9bb	\|- ( ( e = E /\ f = F ) -> ( ta <-> ze ) )
51	49 50	sylbi	\|- ( <. e , f >. = <. E , F >. -> ( ta <-> ze ) )
52		vex	\|- g e. _V
53		vex	\|- h e. _V
54	52 53	opth	\|- ( <. g , h >. = <. G , H >. <-> ( g = G /\ h = H ) )
55	7 8	sylan9bb	\|- ( ( g = G /\ h = H ) -> ( ze <-> rh ) )
56	54 55	sylbi	\|- ( <. g , h >. = <. G , H >. -> ( ze <-> rh ) )
57	51 56	sylan9bb	\|- ( ( <. e , f >. = <. E , F >. /\ <. g , h >. = <. G , H >. ) -> ( ta <-> rh ) )
58	46 57	sylbi	\|- ( <. <. e , f >. , <. g , h >. >. = <. <. E , F >. , <. G , H >. >. -> ( ta <-> rh ) )
59	58	eqcoms	\|- ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. -> ( ta <-> rh ) )
60	43 59	sylan9bb	\|- ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. ) -> ( ph <-> rh ) )
61	60	biimp3a	\|- ( ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. /\ <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. /\ ph ) -> rh )
62	61	a1i	\|- ( ( ( ( ( ( ( ( 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 ) )
63	62	rexlimdva	\|- ( ( ( ( ( ( ( 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 ) )
64	63	rexlimdvva	\|- ( ( ( ( ( ( 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 ) )
65	64	rexlimdvva	\|- ( ( ( ( ( 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 ) )
66	65	rexlimdvva	\|- ( ( ( ( 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 ) )
67	66	rexlimdvva	\|- ( ( ( 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 ) )
68		simpl11	\|- ( ( ( ( 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 )
69		simpl12	\|- ( ( ( ( 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 )
70		simpl13	\|- ( ( ( ( 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 )
71		simpl21	\|- ( ( ( ( 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 )
72		simpl22	\|- ( ( ( ( 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 )
73		simpl23	\|- ( ( ( ( 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 )
74		simpl31	\|- ( ( ( ( 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 )
75		simpl32	\|- ( ( ( ( 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 )
76		simpl33	\|- ( ( ( ( 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 )
77		eqidd	\|- ( ( ( ( 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 >. >. )
78		eqidd	\|- ( ( ( ( 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 >. >. )
79		simpr	\|- ( ( ( ( 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 )
80		opeq1	\|- ( g = G -> <. g , h >. = <. G , h >. )
81	80	opeq2d	\|- ( g = G -> <. <. E , F >. , <. g , h >. >. = <. <. E , F >. , <. G , h >. >. )
82	81	eqeq2d	\|- ( g = G -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. ) )
83	82 7	3anbi23d	\|- ( 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 ) ) )
84		opeq2	\|- ( h = H -> <. G , h >. = <. G , H >. )
85	84	opeq2d	\|- ( h = H -> <. <. E , F >. , <. G , h >. >. = <. <. E , F >. , <. G , H >. >. )
86	85	eqeq2d	\|- ( h = H -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. G , H >. >. ) )
87	86 8	3anbi23d	\|- ( 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 ) ) )
88	83 87	rspc2ev	\|- ( ( 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 ) )
89	75 76 77 78 79 88	syl113anc	\|- ( ( ( ( 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 ) )
90		opeq2	\|- ( d = D -> <. C , d >. = <. C , D >. )
91	90	opeq2d	\|- ( d = D -> <. <. A , B >. , <. C , d >. >. = <. <. A , B >. , <. C , D >. >. )
92	91	eqeq2d	\|- ( d = D -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , D >. >. ) )
93	92 4	3anbi13d	\|- ( 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 ) ) )
94	93	2rexbidv	\|- ( 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 ) ) )
95		opeq1	\|- ( e = E -> <. e , f >. = <. E , f >. )
96	95	opeq1d	\|- ( e = E -> <. <. e , f >. , <. g , h >. >. = <. <. E , f >. , <. g , h >. >. )
97	96	eqeq2d	\|- ( e = E -> ( <. <. E , F >. , <. G , H >. >. = <. <. e , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. ) )
98	97 5	3anbi23d	\|- ( 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 ) ) )
99	98	2rexbidv	\|- ( 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 ) ) )
100		opeq2	\|- ( f = F -> <. E , f >. = <. E , F >. )
101	100	opeq1d	\|- ( f = F -> <. <. E , f >. , <. g , h >. >. = <. <. E , F >. , <. g , h >. >. )
102	101	eqeq2d	\|- ( f = F -> ( <. <. E , F >. , <. G , H >. >. = <. <. E , f >. , <. g , h >. >. <-> <. <. E , F >. , <. G , H >. >. = <. <. E , F >. , <. g , h >. >. ) )
103	102 6	3anbi23d	\|- ( 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 ) ) )
104	103	2rexbidv	\|- ( 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 ) ) )
105	94 99 104	rspc3ev	\|- ( ( ( 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 ) )
106	72 73 74 89 105	syl31anc	\|- ( ( ( ( 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 ) )
107		opeq1	\|- ( a = A -> <. a , b >. = <. A , b >. )
108	107	opeq1d	\|- ( a = A -> <. <. a , b >. , <. c , d >. >. = <. <. A , b >. , <. c , d >. >. )
109	108	eqeq2d	\|- ( a = A -> ( <. <. A , B >. , <. C , D >. >. = <. <. a , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. ) )
110	109 1	3anbi13d	\|- ( 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 ) ) )
111	110	rexbidv	\|- ( 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 ) ) )
112	111	2rexbidv	\|- ( 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 ) ) )
113	112	2rexbidv	\|- ( 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 ) ) )
114		opeq2	\|- ( b = B -> <. A , b >. = <. A , B >. )
115	114	opeq1d	\|- ( b = B -> <. <. A , b >. , <. c , d >. >. = <. <. A , B >. , <. c , d >. >. )
116	115	eqeq2d	\|- ( b = B -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , b >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. ) )
117	116 2	3anbi13d	\|- ( 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 ) ) )
118	117	rexbidv	\|- ( 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 ) ) )
119	118	2rexbidv	\|- ( 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 ) ) )
120	119	2rexbidv	\|- ( 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 ) ) )
121		opeq1	\|- ( c = C -> <. c , d >. = <. C , d >. )
122	121	opeq2d	\|- ( c = C -> <. <. A , B >. , <. c , d >. >. = <. <. A , B >. , <. C , d >. >. )
123	122	eqeq2d	\|- ( c = C -> ( <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. c , d >. >. <-> <. <. A , B >. , <. C , D >. >. = <. <. A , B >. , <. C , d >. >. ) )
124	123 3	3anbi13d	\|- ( 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 ) ) )
125	124	rexbidv	\|- ( 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 ) ) )
126	125	2rexbidv	\|- ( 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 ) ) )
127	126	2rexbidv	\|- ( 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 ) ) )
128	113 120 127	rspc3ev	\|- ( ( ( 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 ) )
129	69 70 71 106 128	syl31anc	\|- ( ( ( ( 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 ) )
130	9	rexeqdv	\|- ( 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 ) ) )
131	9 130	rexeqbidv	\|- ( 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 ) ) )
132	9 131	rexeqbidv	\|- ( 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 ) ) )
133	9 132	rexeqbidv	\|- ( 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 ) ) )
134	9 133	rexeqbidv	\|- ( 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 ) ) )
135	9 134	rexeqbidv	\|- ( 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 ) ) )
136	9 135	rexeqbidv	\|- ( 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 ) ) )
137	9 136	rexeqbidv	\|- ( 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 ) ) )
138	137	rspcev	\|- ( ( 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 ) )
139	68 129 138	syl2anc	\|- ( ( ( ( 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 ) )
140	139	ex	\|- ( ( ( 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 ) ) )
141	67 140	impbid	\|- ( ( ( 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 ) )
142	27 141	bitrid	\|- ( ( ( 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 ) )

Metamath Proof Explorer

Theorem br8

Proof