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

Theorem csbingVD 28933
Description: Virtual deduction proof of csbing 3540. 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. csbing 3540 is csbingVD 28933 without virtual deductions and was automatically derived from csbingVD 28933.
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 28602 . . . . . 6  |-  (. A  e.  B  ->.  A  e.  B ).
2 df-in 3319 . . . . . . . 8  |-  ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
32ax-gen 1555 . . . . . . 7  |-  A. x
( C  i^i  D
)  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
4 spsbc 3165 . . . . . . 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 28732 . . . . . 6  |-  (. A  e.  B  ->.  [. A  /  x ]. ( C  i^i  D
)  =  { y  |  ( y  e.  C  /\  y  e.  D ) } ).
6 sbceqg 3259 . . . . . . 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 199 . . . . . 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 28726 . . . . 5  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) } ).
9 csbabg 3302 . . . . . 6  |-  ( A  e.  B  ->  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) } )
101, 9e1_ 28665 . . . . 5  |-  (. A  e.  B  ->.  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D
) } ).
11 eqeq1 2441 . . . . . 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 215 . . . . 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 28726 . . . 4  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
14 sbcang 3196 . . . . . . . 8  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D
)  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) )
151, 14e1_ 28665 . . . . . . 7  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) ).
16 sbcel2g 3264 . . . . . . . . 9  |-  ( A  e.  B  ->  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) )
171, 16e1_ 28665 . . . . . . . 8  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C
) ).
18 sbcel2g 3264 . . . . . . . . 9  |-  ( A  e.  B  ->  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) )
191, 18e1_ 28665 . . . . . . . 8  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D
) ).
20 pm4.38 843 . . . . . . . . 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 424 . . . . . . . 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 28726 . . . . . . 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 318 . . . . . . . 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 215 . . . . . . 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 28726 . . . . . 6  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
2625gen11 28654 . . . . 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 2545 . . . . . 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 187 . . . . 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_ 28665 . . . 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 2441 . . . . 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 215 . . . 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 28726 . . 3  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
33 df-in 3319 . . 3  |-  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  =  {
y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }
34 eqeq2 2444 . . . 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 217 . . 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 28732 . 2  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) ).
3736in1 28599 1  |-  ( A  e.  B  ->  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549    = wceq 1652    e. wcel 1725   {cab 2421   [.wsbc 3153   [_csb 3243    i^i cin 3311
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sbc 3154  df-csb 3244  df-in 3319  df-vd1 28598
  Copyright terms: Public domain W3C validator