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

Theorem csbingVD 31454
Description: Virtual deduction proof of csbingOLD 3710. 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. csbingOLD 3710 is csbingVD 31454 without virtual deductions and was automatically derived from csbingVD 31454.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2::  |-  ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D )  }
20:2:  |-  A. x ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
30:1,20:  |-  (. A  e.  B  ->.  [. A  /  x ]. ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) } ).
3:1,30:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) } ).
4:1:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
5:3,4:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
6:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) ).
7:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) ).
8:6,7:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D )  ) ).
9:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) ).
10:9,8:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
11:10:  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
12:11:  |-  (. A  e.  B  ->.  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) }  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
13:5,12:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
14::  |-  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  =  {  y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }
15:13,14:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) ).
qed:15:  |-  ( A  e.  B  ->  [_ A  /  x ]_ ( C  i^i  D )  =  (  [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbingVD  |-  ( A  e.  B  ->  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) )

Proof of Theorem csbingVD
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 idn1 31120 . . . . . 6  |-  (. A  e.  B  ->.  A  e.  B ).
2 df-in 3332 . . . . . . . 8  |-  ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
32ax-gen 1596 . . . . . . 7  |-  A. x
( C  i^i  D
)  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
4 spsbc 3196 . . . . . . 7  |-  ( A  e.  B  ->  ( A. x ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) }  ->  [. A  /  x ]. ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D
) } ) )
51, 3, 4e10 31250 . . . . . 6  |-  (. A  e.  B  ->.  [. A  /  x ]. ( C  i^i  D
)  =  { y  |  ( y  e.  C  /\  y  e.  D ) } ).
6 sbceqg 3674 . . . . . . 7  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( C  i^i  D
)  =  { y  |  ( y  e.  C  /\  y  e.  D ) }  <->  [_ A  /  x ]_ ( C  i^i  D )  =  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) } ) )
76biimpd 207 . . . . . 6  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( C  i^i  D
)  =  { y  |  ( y  e.  C  /\  y  e.  D ) }  ->  [_ A  /  x ]_ ( C  i^i  D )  =  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D
) } ) )
81, 5, 7e11 31244 . . . . 5  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) } ).
9 csbabgOLD 3705 . . . . . 6  |-  ( A  e.  B  ->  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) } )
101, 9e1_ 31183 . . . . 5  |-  (. A  e.  B  ->.  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D
) } ).
11 eqeq1 2447 . . . . . 6  |-  ( [_ A  /  x ]_ ( C  i^i  D )  = 
[_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  ->  ( [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) } 
<-> 
[_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D
) } ) )
1211biimprd 223 . . . . 5  |-  ( [_ A  /  x ]_ ( C  i^i  D )  = 
[_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  ->  ( [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) }  ->  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ) )
138, 10, 12e11 31244 . . . 4  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
14 sbcangOLD 3227 . . . . . . . 8  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D
)  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) )
151, 14e1_ 31183 . . . . . . 7  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) ).
16 sbcel2gOLD 3681 . . . . . . . . 9  |-  ( A  e.  B  ->  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) )
171, 16e1_ 31183 . . . . . . . 8  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C
) ).
18 sbcel2gOLD 3681 . . . . . . . . 9  |-  ( A  e.  B  ->  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) )
191, 18e1_ 31183 . . . . . . . 8  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D
) ).
20 pm4.38 862 . . . . . . . . 9  |-  ( ( ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C )  /\  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) )  ->  ( ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) )
2120ex 434 . . . . . . . 8  |-  ( (
[. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C )  -> 
( ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D
)  ->  ( ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D
)  <->  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ) )
2217, 19, 21e11 31244 . . . . . . 7  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
23 bibi1 327 . . . . . . . 8  |-  ( (
[. A  /  x ]. ( y  e.  C  /\  y  e.  D
)  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) )  -> 
( ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) )  <->  ( ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D
)  <->  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ) )
2423biimprd 223 . . . . . . 7  |-  ( (
[. A  /  x ]. ( y  e.  C  /\  y  e.  D
)  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) )  -> 
( ( ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) )  -> 
( [. A  /  x ]. ( y  e.  C  /\  y  e.  D
)  <->  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ) )
2515, 22, 24e11 31244 . . . . . 6  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
2625gen11 31172 . . . . 5  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. (
y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
27 abbi 2551 . . . . . 6  |-  ( A. y ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) )  <->  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D
) }  =  {
y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } )
2827biimpi 194 . . . . 5  |-  ( A. y ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) )  ->  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) }  =  { y  |  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } )
2926, 28e1_ 31183 . . . 4  |-  (. A  e.  B  ->.  { y  | 
[. A  /  x ]. ( y  e.  C  /\  y  e.  D
) }  =  {
y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
30 eqeq1 2447 . . . . 5  |-  ( [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) }  ->  ( [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }  <->  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) }  =  { y  |  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ) )
3130biimprd 223 . . . 4  |-  ( [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) }  ->  ( { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) }  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }  ->  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ) )
3213, 29, 31e11 31244 . . 3  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
33 df-in 3332 . . 3  |-  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  =  {
y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }
34 eqeq2 2450 . . . 4  |-  ( (
[_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }  ->  ( [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  <->  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ) )
3534biimprcd 225 . . 3  |-  ( [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }  ->  ( ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  =  {
y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }  ->  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) ) )
3632, 33, 35e10 31250 . 2  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) ).
3736in1 31117 1  |-  ( A  e.  B  ->  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1362    = wceq 1364    e. wcel 1761   {cab 2427   [.wsbc 3183   [_csb 3285    i^i cin 3324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-sbc 3184  df-csb 3286  df-in 3332  df-vd1 31116
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator