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

Theorem csbunigVD 36935
Description: Virtual deduction proof of csbunigOLD 36852. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbunigOLD 36852 is csbunigVD 36935 without virtual deductions and was automatically derived from csbunigVD 36935.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
3:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  B  <->  y  e.  [_ A  /  x ]_ B ) ).
4:2,3:  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
5:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B ) ) ).
6:4,5:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
7:6:  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
8:7:  |-  (. A  e.  V  ->.  ( E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
9:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B ) ) ).
10:8,9:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
11:10:  |-  (. A  e.  V  ->.  A. z ( [. A  /  x ]. E. y (  z  e.  y  /\  y  e.  B )  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
12:11:  |-  (. A  e.  V  ->.  { z  |  [. A  /  x ]. E. y (  z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) } ).
13:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) }  ).
14:12,13:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) } ).
15::  |-  U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) }
16:15:  |-  A. x U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) }
17:1,16:  |-  (. A  e.  V  ->.  [. A  /  x ]. U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) } ).
18:1,17:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) } ).
19:14,18:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) } ).
20::  |-  U. [_ A  /  x ]_ B  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) }
21:19,20:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B ).
qed:21:  |-  ( A  e.  V  ->  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbunigVD  |-  ( A  e.  V  ->  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B )

Proof of Theorem csbunigVD
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 36582 . . . . . . . . . . . . 13  |-  (. A  e.  V  ->.  A  e.  V ).
2 sbcg 3371 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
31, 2e1a 36644 . . . . . . . . . . . 12  |-  (. A  e.  V  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
4 sbcel2gOLD 36543 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  e.  B  <->  y  e.  [_ A  /  x ]_ B ) )
51, 4e1a 36644 . . . . . . . . . . . 12  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  B  <->  y  e.  [_ A  /  x ]_ B
) ).
6 pm4.38 880 . . . . . . . . . . . . 13  |-  ( ( ( [. A  /  x ]. z  e.  y  <-> 
z  e.  y )  /\  ( [. A  /  x ]. y  e.  B  <->  y  e.  [_ A  /  x ]_ B
) )  ->  (
( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B
)  <->  ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) ) )
76ex 435 . . . . . . . . . . . 12  |-  ( (
[. A  /  x ]. z  e.  y  <->  z  e.  y )  -> 
( ( [. A  /  x ]. y  e.  B  <->  y  e.  [_ A  /  x ]_ B
)  ->  ( ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B
)  <->  ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) ) ) )
83, 5, 7e11 36705 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
9 sbcangOLD 36527 . . . . . . . . . . . 12  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B
)  <->  ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B ) ) )
101, 9e1a 36644 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B ) ) ).
11 bibi1 328 . . . . . . . . . . . 12  |-  ( (
[. A  /  x ]. ( z  e.  y  /\  y  e.  B
)  <->  ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B ) )  -> 
( ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) )  <->  ( ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B
)  <->  ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) ) ) )
1211biimprcd 228 . . . . . . . . . . 11  |-  ( ( ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B
)  <->  ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) )  -> 
( ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B ) )  -> 
( [. A  /  x ]. ( z  e.  y  /\  y  e.  B
)  <->  ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) ) ) )
138, 10, 12e11 36705 . . . . . . . . . 10  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
1413gen11 36633 . . . . . . . . 9  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. (
z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
15 exbi 1713 . . . . . . . . 9  |-  ( A. y ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) )  -> 
( E. y [. A  /  x ]. (
z  e.  y  /\  y  e.  B )  <->  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) ) )
1614, 15e1a 36644 . . . . . . . 8  |-  (. A  e.  V  ->.  ( E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B
)  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
17 sbcexgOLD 36541 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B
) ) )
181, 17e1a 36644 . . . . . . . 8  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y
( z  e.  y  /\  y  e.  B
)  <->  E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B ) ) ).
19 bibi1 328 . . . . . . . . 9  |-  ( (
[. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B
) )  ->  (
( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) )  <->  ( E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B
)  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ) )
2019biimprcd 228 . . . . . . . 8  |-  ( ( E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) )  ->  (
( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B
) )  ->  ( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) ) ) )
2116, 18, 20e11 36705 . . . . . . 7  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y
( z  e.  y  /\  y  e.  B
)  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
2221gen11 36633 . . . . . 6  |-  (. A  e.  V  ->.  A. z ( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) ) ).
23 abbi 2560 . . . . . . 7  |-  ( A. z ( [. A  /  x ]. E. y
( z  e.  y  /\  y  e.  B
)  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) )  <->  { z  |  [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) } )
2423biimpi 197 . . . . . 6  |-  ( A. z ( [. A  /  x ]. E. y
( z  e.  y  /\  y  e.  B
)  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) )  ->  { z  |  [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) } )
2522, 24e1a 36644 . . . . 5  |-  (. A  e.  V  ->.  { z  | 
[. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) } ).
26 csbabgOLD 36851 . . . . . 6  |-  ( A  e.  V  ->  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) } )
271, 26e1a 36644 . . . . 5  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) } ).
28 eqeq2 2444 . . . . . 6  |-  ( { z  |  [. A  /  x ]. E. y
( z  e.  y  /\  y  e.  B
) }  =  {
z  |  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) }  ->  ( [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) }  <->  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) } ) )
2928biimpd 210 . . . . 5  |-  ( { z  |  [. A  /  x ]. E. y
( z  e.  y  /\  y  e.  B
) }  =  {
z  |  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) }  ->  ( [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) }  ->  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) } ) )
3025, 27, 29e11 36705 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) } ).
31 df-uni 4223 . . . . . . 7  |-  U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) }
3231ax-gen 1665 . . . . . 6  |-  A. x U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  B
) }
33 spsbc 3318 . . . . . 6  |-  ( A  e.  V  ->  ( A. x U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  ->  [. A  /  x ]. U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  B
) } ) )
341, 32, 33e10 36711 . . . . 5  |-  (. A  e.  V  ->.  [. A  /  x ]. U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  B
) } ).
35 sbceqg 3807 . . . . . 6  |-  ( A  e.  V  ->  ( [. A  /  x ]. U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  B
) }  <->  [_ A  /  x ]_ U. B  = 
[_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) } ) )
3635biimpd 210 . . . . 5  |-  ( A  e.  V  ->  ( [. A  /  x ]. U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  B
) }  ->  [_ A  /  x ]_ U. B  =  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) } ) )
371, 34, 36e11 36705 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  [_ A  /  x ]_ {
z  |  E. y
( z  e.  y  /\  y  e.  B
) } ).
38 eqeq2 2444 . . . . 5  |-  ( [_ A  /  x ]_ {
z  |  E. y
( z  e.  y  /\  y  e.  B
) }  =  {
z  |  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) }  ->  ( [_ A  /  x ]_ U. B  =  [_ A  /  x ]_ {
z  |  E. y
( z  e.  y  /\  y  e.  B
) }  <->  [_ A  /  x ]_ U. B  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) } ) )
3938biimpd 210 . . . 4  |-  ( [_ A  /  x ]_ {
z  |  E. y
( z  e.  y  /\  y  e.  B
) }  =  {
z  |  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) }  ->  ( [_ A  /  x ]_ U. B  =  [_ A  /  x ]_ {
z  |  E. y
( z  e.  y  /\  y  e.  B
) }  ->  [_ A  /  x ]_ U. B  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) } ) )
4030, 37, 39e11 36705 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) } ).
41 df-uni 4223 . . 3  |-  U. [_ A  /  x ]_ B  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) }
42 eqeq2 2444 . . . 4  |-  ( U. [_ A  /  x ]_ B  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) }  ->  (
[_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B 
<-> 
[_ A  /  x ]_ U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) } ) )
4342biimprcd 228 . . 3  |-  ( [_ A  /  x ]_ U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) }  ->  ( U. [_ A  /  x ]_ B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) }  ->  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B ) )
4440, 41, 43e10 36711 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B ).
4544in1 36579 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437   E.wex 1659    e. wcel 1870   {cab 2414   [.wsbc 3305   [_csb 3401   U.cuni 4222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-sbc 3306  df-csb 3402  df-uni 4223  df-vd1 36578
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator