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

Theorem csbunigVD 29010
Description: Virtual deduction proof of csbunig 4023. 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. csbunig 4023 is csbunigVD 29010 without virtual deductions and was automatically derived from csbunigVD 29010.
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 28665 . . . . . . . . . . . . 13  |-  (. A  e.  V  ->.  A  e.  V ).
2 sbcg 3226 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) )
31, 2e1_ 28728 . . . . . . . . . . . 12  |-  (. A  e.  V  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
4 sbcel2g 3272 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  e.  B  <->  y  e.  [_ A  /  x ]_ B ) )
51, 4e1_ 28728 . . . . . . . . . . . 12  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  B  <->  y  e.  [_ A  /  x ]_ B
) ).
6 pm4.38 843 . . . . . . . . . . . . 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 424 . . . . . . . . . . . 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 28789 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
9 sbcang 3204 . . . . . . . . . . . 12  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B
)  <->  ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B ) ) )
101, 9e1_ 28728 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B ) ) ).
11 bibi1 318 . . . . . . . . . . . 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 217 . . . . . . . . . . 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 28789 . . . . . . . . . 10  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
1413gen11 28717 . . . . . . . . 9  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. (
z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
15 exbi 1591 . . . . . . . . 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, 15e1_ 28728 . . . . . . . 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 sbcexg 3211 . . . . . . . . 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, 17e1_ 28728 . . . . . . . 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 318 . . . . . . . . 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 217 . . . . . . . 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 28789 . . . . . . 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 28717 . . . . . 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 2546 . . . . . . 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 187 . . . . . 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, 24e1_ 28728 . . . . 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 csbabg 3310 . . . . . 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, 26e1_ 28728 . . . . 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 2445 . . . . . 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 199 . . . . 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 28789 . . . 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 4016 . . . . . . 7  |-  U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) }
3231ax-gen 1555 . . . . . 6  |-  A. x U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  B
) }
33 spsbc 3173 . . . . . 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 28795 . . . . 5  |-  (. A  e.  V  ->.  [. A  /  x ]. U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  B
) } ).
35 sbceqg 3267 . . . . . 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 199 . . . . 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 28789 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  [_ A  /  x ]_ {
z  |  E. y
( z  e.  y  /\  y  e.  B
) } ).
38 eqeq2 2445 . . . . 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 199 . . . 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 28789 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  {
z  |  E. y
( z  e.  y  /\  y  e.  [_ A  /  x ]_ B
) } ).
41 df-uni 4016 . . 3  |-  U. [_ A  /  x ]_ B  =  { z  |  E. y ( z  e.  y  /\  y  e. 
[_ A  /  x ]_ B ) }
42 eqeq2 2445 . . . 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 217 . . 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 28795 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B ).
4544in1 28662 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725   {cab 2422   [.wsbc 3161   [_csb 3251   U.cuni 4015
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-sbc 3162  df-csb 3252  df-uni 4016  df-vd1 28661
  Copyright terms: Public domain W3C validator