Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  csbxpgVD Unicode version

Theorem csbxpgVD 28986
Description: Virtual deduction proof of csbxpg 4732. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbxpg 4732 is csbxpgVD 28986 without virtual deductions and was automatically derived from csbxpgVD 28986.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. w  e.  B  <->  [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B ) ).
3:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ w  =  w ).
4:3:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B  <->  w  e.  [_ A  /  x ]_ B ) ).
5:2,4:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. w  e.  B  <->  w  e.  [_ A  /  x ]_ B ) ).
6:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  C  <->  [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C ) ).
7:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ y  =  y ).
8:7:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C  <->  y  e.  [_ A  /  x ]_ C ) ).
9:6,8:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) ).
10:5,9:  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ).
11:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C )  <->  ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C ) ) ).
12:10,11:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ).
13:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. z  =  <. w ,.  y >.  <->  z  =  <. w ,  y >. ) ).
14:12,13:  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. z  =  <. w  ,. y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
15:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  =  <. w  ,. y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( [. A  /  x ]. z  =  <. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) ) ) ).
16:14,15:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  =  <. w  ,. y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
17:16:  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
18:17:  |-  (. A  e.  V  ->.  ( E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
19:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) ) ).
20:18,19:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
21:20:  |-  (. A  e.  V  ->.  A. w ( [. A  /  x ]. E. y (  z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
22:21:  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. E. y (  z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
23:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w E. y (  z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w [. A  /  x ]. E. y  ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) ) ).
24:22,23:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w E. y (  z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
25:24:  |-  (. A  e.  V  ->.  A. z ( [. A  /  x ]. E. w E.  y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
26:25:  |-  (. A  e.  V  ->.  { z  |  [. A  /  x ]. E. w E.  y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  E. w E. y (  z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ).
27:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. w E.  y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  [. A  /  x ].  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) } ).
28:26,27:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. w E.  y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  E. w E. y (  z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ).
29::  |-  { <. w ,. y >.  |  ( w  e.  B  /\  y  e.  C ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }
30::  |-  ( B  X.  C )  =  { <. w ,. y >.  |  ( w  e.  B  /\  y  e.  C ) }
31:29,30:  |-  ( B  X.  C )  =  { z  |  E. w E. y ( z  =  <. w  ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }
32:31:  |-  A. x ( B  X.  C )  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }
33:1,32:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C )  =  [_ A  /  x ]_ { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) } ).
34:28,33:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C )  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ).
35::  |-  { <. w ,. y >.  |  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }
36::  |-  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C )  =  {  <. w ,  y >.  |  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) }
37:35,36:  |-  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C )  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }
38:34,37:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C )  =  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C ) ).
qed:38:  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  X.  C )  =  (  [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbxpgVD  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  X.  C )  =  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C
) )

Proof of Theorem csbxpgVD
Dummy variables  w  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 28641 . . . . . . . . . . . . . . . . . . 19  |-  (. A  e.  V  ->.  A  e.  V ).
2 sbcel12g 3109 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  V  ->  ( [. A  /  x ]. w  e.  B  <->  [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B ) )
31, 2e1_ 28704 . . . . . . . . . . . . . . . . . 18  |-  (. A  e.  V  ->.  ( [. A  /  x ]. w  e.  B  <->  [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B ) ).
4 csbconstg 3108 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  V  ->  [_ A  /  x ]_ w  =  w )
51, 4e1_ 28704 . . . . . . . . . . . . . . . . . . 19  |-  (. A  e.  V  ->.  [_ A  /  x ]_ w  =  w ).
6 eleq1 2356 . . . . . . . . . . . . . . . . . . 19  |-  ( [_ A  /  x ]_ w  =  w  ->  ( [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B  <->  w  e.  [_ A  /  x ]_ B ) )
75, 6e1_ 28704 . . . . . . . . . . . . . . . . . 18  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ w  e. 
[_ A  /  x ]_ B  <->  w  e.  [_ A  /  x ]_ B ) ).
8 bibi1 317 . . . . . . . . . . . . . . . . . . 19  |-  ( (
[. A  /  x ]. w  e.  B  <->  [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B )  -> 
( ( [. A  /  x ]. w  e.  B  <->  w  e.  [_ A  /  x ]_ B )  <-> 
( [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B  <->  w  e.  [_ A  /  x ]_ B ) ) )
98biimprd 214 . . . . . . . . . . . . . . . . . 18  |-  ( (
[. A  /  x ]. w  e.  B  <->  [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B )  -> 
( ( [_ A  /  x ]_ w  e. 
[_ A  /  x ]_ B  <->  w  e.  [_ A  /  x ]_ B )  ->  ( [. A  /  x ]. w  e.  B  <->  w  e.  [_ A  /  x ]_ B ) ) )
103, 7, 9e11 28765 . . . . . . . . . . . . . . . . 17  |-  (. A  e.  V  ->.  ( [. A  /  x ]. w  e.  B  <->  w  e.  [_ A  /  x ]_ B ) ).
11 sbcel12g 3109 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  e.  C  <->  [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C ) )
121, 11e1_ 28704 . . . . . . . . . . . . . . . . . 18  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  C  <->  [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C ) ).
13 csbconstg 3108 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  V  ->  [_ A  /  x ]_ y  =  y )
141, 13e1_ 28704 . . . . . . . . . . . . . . . . . . 19  |-  (. A  e.  V  ->.  [_ A  /  x ]_ y  =  y ).
15 eleq1 2356 . . . . . . . . . . . . . . . . . . 19  |-  ( [_ A  /  x ]_ y  =  y  ->  ( [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C  <->  y  e.  [_ A  /  x ]_ C
) )
1614, 15e1_ 28704 . . . . . . . . . . . . . . . . . 18  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ y  e. 
[_ A  /  x ]_ C  <->  y  e.  [_ A  /  x ]_ C
) ).
17 bibi1 317 . . . . . . . . . . . . . . . . . . 19  |-  ( (
[. A  /  x ]. y  e.  C  <->  [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C )  -> 
( ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C
)  <->  ( [_ A  /  x ]_ y  e. 
[_ A  /  x ]_ C  <->  y  e.  [_ A  /  x ]_ C
) ) )
1817biimprd 214 . . . . . . . . . . . . . . . . . 18  |-  ( (
[. A  /  x ]. y  e.  C  <->  [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C )  -> 
( ( [_ A  /  x ]_ y  e. 
[_ A  /  x ]_ C  <->  y  e.  [_ A  /  x ]_ C
)  ->  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C
) ) )
1912, 16, 18e11 28765 . . . . . . . . . . . . . . . . 17  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C
) ).
20 pm4.38 842 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( [. A  /  x ]. w  e.  B  <->  w  e.  [_ A  /  x ]_ B )  /\  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) )  ->  ( ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )
2120ex 423 . . . . . . . . . . . . . . . . 17  |-  ( (
[. A  /  x ]. w  e.  B  <->  w  e.  [_ A  /  x ]_ B )  -> 
( ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C
)  ->  ( ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C
)  <->  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) )
2210, 19, 21e11 28765 . . . . . . . . . . . . . . . 16  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ).
23 sbcang 3047 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C
)  <->  ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C ) ) )
241, 23e1_ 28704 . . . . . . . . . . . . . . . 16  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C )  <->  ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C ) ) ).
25 bibi1 317 . . . . . . . . . . . . . . . . 17  |-  ( (
[. A  /  x ]. ( w  e.  B  /\  y  e.  C
)  <->  ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C ) )  -> 
( ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) )  <->  ( ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C
)  <->  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) )
2625biimprcd 216 . . . . . . . . . . . . . . . 16  |-  ( ( ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C
)  <->  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) )  -> 
( ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C )  <->  ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C ) )  -> 
( [. A  /  x ]. ( w  e.  B  /\  y  e.  C
)  <->  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) )
2722, 24, 26e11 28765 . . . . . . . . . . . . . . 15  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ).
28 sbcg 3069 . . . . . . . . . . . . . . . 16  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  =  <. w ,  y >.  <->  z  =  <. w ,  y >.
) )
291, 28e1_ 28704 . . . . . . . . . . . . . . 15  |-  (. A  e.  V  ->.  ( [. A  /  x ]. z  = 
<. w ,  y >.  <->  z  =  <. w ,  y
>. ) ).
30 pm4.38 842 . . . . . . . . . . . . . . . 16  |-  ( ( ( [. A  /  x ]. z  =  <. w ,  y >.  <->  z  =  <. w ,  y >.
)  /\  ( [. A  /  x ]. (
w  e.  B  /\  y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  ->  ( ( [. A  /  x ]. z  =  <. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) )
3130expcom 424 . . . . . . . . . . . . . . 15  |-  ( (
[. A  /  x ]. ( w  e.  B  /\  y  e.  C
)  <->  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) )  -> 
( ( [. A  /  x ]. z  = 
<. w ,  y >.  <->  z  =  <. w ,  y
>. )  ->  ( (
[. A  /  x ]. z  =  <. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ) )
3227, 29, 31e11 28765 . . . . . . . . . . . . . 14  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. z  =  <. w ,  y
>.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
33 sbcang 3047 . . . . . . . . . . . . . . 15  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  ( [. A  /  x ]. z  = 
<. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C
) ) ) )
341, 33e1_ 28704 . . . . . . . . . . . . . 14  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( [. A  /  x ]. z  =  <. w ,  y
>.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) ) ) ).
35 bibi1 317 . . . . . . . . . . . . . . 15  |-  ( (
[. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  ( [. A  /  x ]. z  = 
<. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C
) ) )  -> 
( ( [. A  /  x ]. ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  <-> 
( ( [. A  /  x ]. z  = 
<. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C
) )  <->  ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ) )
3635biimprcd 216 . . . . . . . . . . . . . 14  |-  ( ( ( [. A  /  x ]. z  =  <. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  ->  ( ( [. A  /  x ]. (
z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  ( [. A  /  x ]. z  = 
<. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C
) ) )  -> 
( [. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ) )
3732, 34, 36e11 28765 . . . . . . . . . . . . 13  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
3837gen11 28693 . . . . . . . . . . . 12  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. (
z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
39 exbi 1571 . . . . . . . . . . . 12  |-  ( A. y ( [. A  /  x ]. ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  ->  ( E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) )
4038, 39e1_ 28704 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
41 sbcexg 3054 . . . . . . . . . . . 12  |-  ( A  e.  V  ->  ( [. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) ) )
421, 41e1_ 28704 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. y [. A  /  x ]. ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) ) ).
43 bibi1 317 . . . . . . . . . . . 12  |-  ( (
[. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) )  ->  (
( [. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  <->  ( E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ) )
4443biimprcd 216 . . . . . . . . . . 11  |-  ( ( E. y [. A  /  x ]. ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  ->  ( ( [. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) )  ->  ( [. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ) )
4540, 42, 44e11 28765 . . . . . . . . . 10  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
4645gen11 28693 . . . . . . . . 9  |-  (. A  e.  V  ->.  A. w ( [. A  /  x ]. E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) )  <->  E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
47 exbi 1571 . . . . . . . . 9  |-  ( A. w ( [. A  /  x ]. E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  ->  ( E. w [. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) )
4846, 47e1_ 28704 . . . . . . . 8  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
49 sbcexg 3054 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. w [. A  /  x ]. E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) ) )
501, 49e1_ 28704 . . . . . . . 8  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) )  <->  E. w [. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) ) ).
51 bibi1 317 . . . . . . . . 9  |-  ( (
[. A  /  x ]. E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. w [. A  /  x ]. E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) )  ->  (
( [. A  /  x ]. E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  <->  ( E. w [. A  /  x ]. E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ) )
5251biimprcd 216 . . . . . . . 8  |-  ( ( E. w [. A  /  x ]. E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  ->  ( ( [. A  /  x ]. E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. w [. A  /  x ]. E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) )  ->  ( [. A  /  x ]. E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
)  <->  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ) )
5348, 50, 52e11 28765 . . . . . . 7  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) )  <->  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
5453gen11 28693 . . . . . 6  |-  (. A  e.  V  ->.  A. z ( [. A  /  x ]. E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
55 abbi 2406 . . . . . . 7  |-  ( A. z ( [. A  /  x ]. E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) )  <->  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  <->  { z  |  [. A  /  x ]. E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) }  =  {
z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } )
5655biimpi 186 . . . . . 6  |-  ( A. z ( [. A  /  x ]. E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) )  <->  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) )  ->  { z  |  [. A  /  x ]. E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } )
5754, 56e1_ 28704 . . . . 5  |-  (. A  e.  V  ->.  { z  | 
[. A  /  x ]. E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) }  =  {
z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ).
58 csbabg 3155 . . . . . 6  |-  ( A  e.  V  ->  [_ A  /  x ]_ { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  =  { z  |  [. A  /  x ]. E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) } )
591, 58e1_ 28704 . . . . 5  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  | 
[. A  /  x ]. E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) } ).
60 eqeq2 2305 . . . . . 6  |-  ( { z  |  [. A  /  x ]. E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ->  ( [_ A  /  x ]_ { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  =  { z  |  [. A  /  x ]. E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }  <->  [_ A  /  x ]_ { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ) )
6160biimpd 198 . . . . 5  |-  ( { z  |  [. A  /  x ]. E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ->  ( [_ A  /  x ]_ { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  =  { z  |  [. A  /  x ]. E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }  ->  [_ A  /  x ]_ { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ) )
6257, 59, 61e11 28765 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ).
63 df-xp 4711 . . . . . . 7  |-  ( B  X.  C )  =  { <. w ,  y
>.  |  ( w  e.  B  /\  y  e.  C ) }
64 df-opab 4094 . . . . . . 7  |-  { <. w ,  y >.  |  ( w  e.  B  /\  y  e.  C ) }  =  { z  |  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  B  /\  y  e.  C )
) }
6563, 64eqtri 2316 . . . . . 6  |-  ( B  X.  C )  =  { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }
6665ax-gen 1536 . . . . 5  |-  A. x
( B  X.  C
)  =  { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }
67 csbeq2g 28614 . . . . 5  |-  ( A  e.  V  ->  ( A. x ( B  X.  C )  =  {
z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  ->  [_ A  /  x ]_ ( B  X.  C
)  =  [_ A  /  x ]_ { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) } ) )
681, 66, 67e10 28772 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C
)  =  [_ A  /  x ]_ { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) } ).
69 eqeq2 2305 . . . . 5  |-  ( [_ A  /  x ]_ {
z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ->  ( [_ A  /  x ]_ ( B  X.  C )  = 
[_ A  /  x ]_ { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }  <->  [_ A  /  x ]_ ( B  X.  C
)  =  { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ) )
7069biimpd 198 . . . 4  |-  ( [_ A  /  x ]_ {
z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C
) ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ->  ( [_ A  /  x ]_ ( B  X.  C )  = 
[_ A  /  x ]_ { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e.  B  /\  y  e.  C ) ) }  ->  [_ A  /  x ]_ ( B  X.  C
)  =  { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ) )
7162, 68, 70e11 28765 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C
)  =  { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ).
72 df-xp 4711 . . . 4  |-  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C )  =  { <. w ,  y >.  |  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) }
73 df-opab 4094 . . . 4  |-  { <. w ,  y >.  |  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) }  =  { z  |  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }
7472, 73eqtri 2316 . . 3  |-  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C )  =  {
z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }
75 eqeq2 2305 . . . 4  |-  ( (
[_ A  /  x ]_ B  X.  [_ A  /  x ]_ C )  =  { z  |  E. w E. y
( z  =  <. w ,  y >.  /\  (
w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ->  ( [_ A  /  x ]_ ( B  X.  C )  =  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C
)  <->  [_ A  /  x ]_ ( B  X.  C
)  =  { z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ) )
7675biimprcd 216 . . 3  |-  ( [_ A  /  x ]_ ( B  X.  C )  =  { z  |  E. w E. y ( z  =  <. w ,  y
>.  /\  ( w  e. 
[_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ->  ( ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C )  =  {
z  |  E. w E. y ( z  = 
<. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ->  [_ A  /  x ]_ ( B  X.  C )  =  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C
) ) )
7771, 74, 76e10 28772 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C
)  =  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C ) ).
7877in1 28638 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  X.  C )  =  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696   {cab 2282   [.wsbc 3004   [_csb 3094   <.cop 3656   {copab 4092    X. cxp 4703
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sbc 3005  df-csb 3095  df-opab 4094  df-xp 4711  df-vd1 28637
  Copyright terms: Public domain W3C validator