Metamath Proof Explorer

Theorem br6

Description: Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013) (Revised by Mario Carneiro, 3-May-2015)

Ref Expression
Hypotheses br6.1 
|- ( a = A -> ( ph <-> ps ) )
br6.2 
|- ( b = B -> ( ps <-> ch ) )
br6.3 
|- ( c = C -> ( ch <-> th ) )
br6.4 
|- ( d = D -> ( th <-> ta ) )
br6.5 
|- ( e = E -> ( ta <-> et ) )
br6.6 
|- ( f = F -> ( et <-> ze ) )
br6.7 
|- ( x = X -> P = Q )
br6.8 
|- 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 ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ph ) }
Assertion br6 
|- ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) -> ( <. A , <. B , C >. >. R <. D , <. E , F >. >. <-> ze ) )

Proof

Step Hyp Ref Expression
1 br6.1 
 |-  ( a = A -> ( ph <-> ps ) )
2 br6.2 
 |-  ( b = B -> ( ps <-> ch ) )
3 br6.3 
 |-  ( c = C -> ( ch <-> th ) )
4 br6.4 
 |-  ( d = D -> ( th <-> ta ) )
5 br6.5 
 |-  ( e = E -> ( ta <-> et ) )
6 br6.6 
 |-  ( f = F -> ( et <-> ze ) )
7 br6.7 
 |-  ( x = X -> P = Q )
8 br6.8 
 |-  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 ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ph ) }
9 opex 
 |-  <. A , <. B , C >. >. e. _V
10 opex 
 |-  <. D , <. E , F >. >. e. _V
11 eqeq1 
 |-  ( p = <. A , <. B , C >. >. -> ( p = <. a , <. b , c >. >. <-> <. A , <. B , C >. >. = <. a , <. b , c >. >. ) )
12 eqcom 
 |-  ( <. A , <. B , C >. >. = <. a , <. b , c >. >. <-> <. a , <. b , c >. >. = <. A , <. B , C >. >. )
13 11 12 bitrdi 
 |-  ( p = <. A , <. B , C >. >. -> ( p = <. a , <. b , c >. >. <-> <. a , <. b , c >. >. = <. A , <. B , C >. >. ) )
14 13 3anbi1d 
 |-  ( p = <. A , <. B , C >. >. -> ( ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ph ) <-> ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) ) )
15 14 rexbidv 
 |-  ( p = <. A , <. B , C >. >. -> ( E. f e. P ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ph ) <-> E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) ) )
16 15 2rexbidv 
 |-  ( p = <. A , <. B , C >. >. -> ( E. d e. P E. e e. P E. f e. P ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ph ) <-> E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) ) )
17 16 2rexbidv 
 |-  ( p = <. A , <. B , C >. >. -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ ph ) <-> E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) ) )
18 17 2rexbidv 
 |-  ( p = <. A , <. B , C >. >. -> ( 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 ( p = <. a , <. b , c >. >. /\ q = <. d , <. e , f >. >. /\ 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) ) )
19 eqeq1 
 |-  ( q = <. D , <. E , F >. >. -> ( q = <. d , <. e , f >. >. <-> <. D , <. E , F >. >. = <. d , <. e , f >. >. ) )
20 eqcom 
 |-  ( <. D , <. E , F >. >. = <. d , <. e , f >. >. <-> <. d , <. e , f >. >. = <. D , <. E , F >. >. )
21 19 20 bitrdi 
 |-  ( q = <. D , <. E , F >. >. -> ( q = <. d , <. e , f >. >. <-> <. d , <. e , f >. >. = <. D , <. E , F >. >. ) )
22 21 3anbi2d 
 |-  ( q = <. D , <. E , F >. >. -> ( ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) <-> ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
23 22 rexbidv 
 |-  ( q = <. D , <. E , F >. >. -> ( E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) <-> E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
24 23 2rexbidv 
 |-  ( q = <. D , <. E , F >. >. -> ( E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) <-> E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
25 24 2rexbidv 
 |-  ( q = <. D , <. E , F >. >. -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ ph ) <-> E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
26 25 2rexbidv 
 |-  ( q = <. D , <. E , F >. >. -> ( 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ q = <. d , <. e , f >. >. /\ 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
27 9 10 18 26 8 brab 
 |-  ( <. A , <. B , C >. >. R <. D , <. E , F >. >. <-> 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) )
28 vex 
 |-  a e. _V
29 opex 
 |-  <. b , c >. e. _V
30 28 29 opth 
 |-  ( <. a , <. b , c >. >. = <. A , <. B , C >. >. <-> ( a = A /\ <. b , c >. = <. B , C >. ) )
31 vex 
 |-  b e. _V
32 vex 
 |-  c e. _V
33 31 32 opth 
 |-  ( <. b , c >. = <. B , C >. <-> ( b = B /\ c = C ) )
34 2 3 sylan9bb 
 |-  ( ( b = B /\ c = C ) -> ( ps <-> th ) )
35 33 34 sylbi 
 |-  ( <. b , c >. = <. B , C >. -> ( ps <-> th ) )
36 1 35 sylan9bb 
 |-  ( ( a = A /\ <. b , c >. = <. B , C >. ) -> ( ph <-> th ) )
37 30 36 sylbi 
 |-  ( <. a , <. b , c >. >. = <. A , <. B , C >. >. -> ( ph <-> th ) )
38 vex 
 |-  d e. _V
39 opex 
 |-  <. e , f >. e. _V
40 38 39 opth 
 |-  ( <. d , <. e , f >. >. = <. D , <. E , F >. >. <-> ( d = D /\ <. e , f >. = <. E , F >. ) )
41 vex 
 |-  e e. _V
42 vex 
 |-  f e. _V
43 41 42 opth 
 |-  ( <. e , f >. = <. E , F >. <-> ( e = E /\ f = F ) )
44 5 6 sylan9bb 
 |-  ( ( e = E /\ f = F ) -> ( ta <-> ze ) )
45 43 44 sylbi 
 |-  ( <. e , f >. = <. E , F >. -> ( ta <-> ze ) )
46 4 45 sylan9bb 
 |-  ( ( d = D /\ <. e , f >. = <. E , F >. ) -> ( th <-> ze ) )
47 40 46 sylbi 
 |-  ( <. d , <. e , f >. >. = <. D , <. E , F >. >. -> ( th <-> ze ) )
48 37 47 sylan9bb 
 |-  ( ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. ) -> ( ph <-> ze ) )
49 48 biimp3a 
 |-  ( ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) -> ze )
50 49 a1i 
 |-  ( ( ( ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) /\ ( x e. S /\ a e. P ) ) /\ ( b e. P /\ c e. P ) ) /\ ( d e. P /\ e e. P ) ) /\ f e. P ) -> ( ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) -> ze ) )
51 50 rexlimdva 
 |-  ( ( ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) /\ ( x e. S /\ a e. P ) ) /\ ( b e. P /\ c e. P ) ) /\ ( d e. P /\ e e. P ) ) -> ( E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) -> ze ) )
52 51 rexlimdvva 
 |-  ( ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) -> ze ) )
53 52 rexlimdvva 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) -> ze ) )
54 53 rexlimdvva 
 |-  ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) -> ze ) )
55 simpl1 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) /\ ze ) -> X e. S )
56 simpl2 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) /\ ze ) -> ( A e. Q /\ B e. Q /\ C e. Q ) )
57 opeq1 
 |-  ( d = D -> <. d , <. e , f >. >. = <. D , <. e , f >. >. )
58 57 eqeq1d 
 |-  ( d = D -> ( <. d , <. e , f >. >. = <. D , <. E , F >. >. <-> <. D , <. e , f >. >. = <. D , <. E , F >. >. ) )
59 58 4 3anbi23d 
 |-  ( d = D -> ( ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ th ) <-> ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. e , f >. >. = <. D , <. E , F >. >. /\ ta ) ) )
60 opeq1 
 |-  ( e = E -> <. e , f >. = <. E , f >. )
61 60 opeq2d 
 |-  ( e = E -> <. D , <. e , f >. >. = <. D , <. E , f >. >. )
62 61 eqeq1d 
 |-  ( e = E -> ( <. D , <. e , f >. >. = <. D , <. E , F >. >. <-> <. D , <. E , f >. >. = <. D , <. E , F >. >. ) )
63 62 5 3anbi23d 
 |-  ( e = E -> ( ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. e , f >. >. = <. D , <. E , F >. >. /\ ta ) <-> ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. E , f >. >. = <. D , <. E , F >. >. /\ et ) ) )
64 opeq2 
 |-  ( f = F -> <. E , f >. = <. E , F >. )
65 64 opeq2d 
 |-  ( f = F -> <. D , <. E , f >. >. = <. D , <. E , F >. >. )
66 65 eqeq1d 
 |-  ( f = F -> ( <. D , <. E , f >. >. = <. D , <. E , F >. >. <-> <. D , <. E , F >. >. = <. D , <. E , F >. >. ) )
67 66 6 3anbi23d 
 |-  ( f = F -> ( ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. E , f >. >. = <. D , <. E , F >. >. /\ et ) <-> ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. E , F >. >. = <. D , <. E , F >. >. /\ ze ) ) )
68 eqid 
 |-  <. A , <. B , C >. >. = <. A , <. B , C >. >.
69 eqid 
 |-  <. D , <. E , F >. >. = <. D , <. E , F >. >.
70 68 69 pm3.2i 
 |-  ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. E , F >. >. = <. D , <. E , F >. >. )
71 df-3an 
 |-  ( ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. E , F >. >. = <. D , <. E , F >. >. /\ ze ) <-> ( ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. E , F >. >. = <. D , <. E , F >. >. ) /\ ze ) )
72 70 71 mpbiran 
 |-  ( ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. E , F >. >. = <. D , <. E , F >. >. /\ ze ) <-> ze )
73 67 72 bitrdi 
 |-  ( f = F -> ( ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. D , <. E , f >. >. = <. D , <. E , F >. >. /\ et ) <-> ze ) )
74 59 63 73 rspc3ev 
 |-  ( ( ( D e. Q /\ E e. Q /\ F e. Q ) /\ ze ) -> E. d e. Q E. e e. Q E. f e. Q ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ th ) )
75 74 3ad2antl3 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) /\ ze ) -> E. d e. Q E. e e. Q E. f e. Q ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ th ) )
76 opeq1 
 |-  ( a = A -> <. a , <. b , c >. >. = <. A , <. b , c >. >. )
77 76 eqeq1d 
 |-  ( a = A -> ( <. a , <. b , c >. >. = <. A , <. B , C >. >. <-> <. A , <. b , c >. >. = <. A , <. B , C >. >. ) )
78 77 1 3anbi13d 
 |-  ( a = A -> ( ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> ( <. A , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ps ) ) )
79 78 rexbidv 
 |-  ( a = A -> ( E. f e. Q ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> E. f e. Q ( <. A , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ps ) ) )
80 79 2rexbidv 
 |-  ( a = A -> ( E. d e. Q E. e e. Q E. f e. Q ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> E. d e. Q E. e e. Q E. f e. Q ( <. A , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ps ) ) )
81 opeq1 
 |-  ( b = B -> <. b , c >. = <. B , c >. )
82 81 opeq2d 
 |-  ( b = B -> <. A , <. b , c >. >. = <. A , <. B , c >. >. )
83 82 eqeq1d 
 |-  ( b = B -> ( <. A , <. b , c >. >. = <. A , <. B , C >. >. <-> <. A , <. B , c >. >. = <. A , <. B , C >. >. ) )
84 83 2 3anbi13d 
 |-  ( b = B -> ( ( <. A , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ps ) <-> ( <. A , <. B , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ch ) ) )
85 84 rexbidv 
 |-  ( b = B -> ( E. f e. Q ( <. A , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ps ) <-> E. f e. Q ( <. A , <. B , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ch ) ) )
86 85 2rexbidv 
 |-  ( b = B -> ( E. d e. Q E. e e. Q E. f e. Q ( <. A , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ps ) <-> E. d e. Q E. e e. Q E. f e. Q ( <. A , <. B , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ch ) ) )
87 opeq2 
 |-  ( c = C -> <. B , c >. = <. B , C >. )
88 87 opeq2d 
 |-  ( c = C -> <. A , <. B , c >. >. = <. A , <. B , C >. >. )
89 88 eqeq1d 
 |-  ( c = C -> ( <. A , <. B , c >. >. = <. A , <. B , C >. >. <-> <. A , <. B , C >. >. = <. A , <. B , C >. >. ) )
90 89 3 3anbi13d 
 |-  ( c = C -> ( ( <. A , <. B , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ch ) <-> ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ th ) ) )
91 90 rexbidv 
 |-  ( c = C -> ( E. f e. Q ( <. A , <. B , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ch ) <-> E. f e. Q ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ th ) ) )
92 91 2rexbidv 
 |-  ( c = C -> ( E. d e. Q E. e e. Q E. f e. Q ( <. A , <. B , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ch ) <-> E. d e. Q E. e e. Q E. f e. Q ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ th ) ) )
93 80 86 92 rspc3ev 
 |-  ( ( ( A e. Q /\ B e. Q /\ C e. Q ) /\ E. d e. Q E. e e. Q E. f e. Q ( <. A , <. B , C >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) )
94 56 75 93 syl2anc 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) /\ ze ) -> E. a e. Q E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) )
95 7 rexeqdv 
 |-  ( x = X -> ( E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> E. f e. Q ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
96 7 95 rexeqbidv 
 |-  ( x = X -> ( E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> E. e e. Q E. f e. Q ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
97 7 96 rexeqbidv 
 |-  ( x = X -> ( E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> E. d e. Q E. e e. Q E. f e. Q ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
98 7 97 rexeqbidv 
 |-  ( x = X -> ( E. c e. P E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> E. c e. Q E. d e. Q E. e e. Q E. f e. Q ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
99 7 98 rexeqbidv 
 |-  ( x = X -> ( E. b e. P E. c e. P E. d e. P E. e e. P E. f e. P ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> E. b e. Q E. c e. Q E. d e. Q E. e e. Q E. f e. Q ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
100 7 99 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
101 100 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) )
102 55 94 101 syl2anc 
 |-  ( ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) /\ ze ) -> 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) )
103 102 ex 
 |-  ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) -> ( ze -> 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) ) )
104 54 103 impbid 
 |-  ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F 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 ( <. a , <. b , c >. >. = <. A , <. B , C >. >. /\ <. d , <. e , f >. >. = <. D , <. E , F >. >. /\ ph ) <-> ze ) )
105 27 104 bitrid 
 |-  ( ( X e. S /\ ( A e. Q /\ B e. Q /\ C e. Q ) /\ ( D e. Q /\ E e. Q /\ F e. Q ) ) -> ( <. A , <. B , C >. >. R <. D , <. E , F >. >. <-> ze ) )