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

Theorem csbingVD 28330
Description: Virtual deduction proof of csbing 3484. 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 3484 is csbingVD 28330 without virtual deductions and was automatically derived from csbingVD 28330.
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 27999 . . . . . 6  |-  (. A  e.  B  ->.  A  e.  B ).
2 df-in 3263 . . . . . . . 8  |-  ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
32ax-gen 1552 . . . . . . 7  |-  A. x
( C  i^i  D
)  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
4 spsbc 3109 . . . . . . 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 28129 . . . . . 6  |-  (. A  e.  B  ->.  [. A  /  x ]. ( C  i^i  D
)  =  { y  |  ( y  e.  C  /\  y  e.  D ) } ).
6 sbceqg 3203 . . . . . . 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 28123 . . . . 5  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) } ).
9 csbabg 3246 . . . . . 6  |-  ( A  e.  B  ->  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. (
y  e.  C  /\  y  e.  D ) } )
101, 9e1_ 28062 . . . . 5  |-  (. A  e.  B  ->.  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D
) } ).
11 eqeq1 2386 . . . . . 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 28123 . . . 4  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
14 sbcang 3140 . . . . . . . 8  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D
)  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) )
151, 14e1_ 28062 . . . . . . 7  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) ).
16 sbcel2g 3208 . . . . . . . . 9  |-  ( A  e.  B  ->  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) )
171, 16e1_ 28062 . . . . . . . 8  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C
) ).
18 sbcel2g 3208 . . . . . . . . 9  |-  ( A  e.  B  ->  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) )
191, 18e1_ 28062 . . . . . . . 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 28123 . . . . . . 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 28123 . . . . . 6  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
2625gen11 28051 . . . . 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 2490 . . . . . 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_ 28062 . . . 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 2386 . . . . 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 28123 . . 3  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  { y  |  ( y  e. 
[_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
33 df-in 3263 . . 3  |-  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  =  {
y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }
34 eqeq2 2389 . . . 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 28129 . 2  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D
)  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) ).
3736in1 27996 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 1546    = wceq 1649    e. wcel 1717   {cab 2366   [.wsbc 3097   [_csb 3187    i^i cin 3255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-sbc 3098  df-csb 3188  df-in 3263  df-vd1 27995
  Copyright terms: Public domain W3C validator