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

Theorem csbfv12gALTVD 28675
Description: Virtual deduction proof of csbfv12gALT 5536. 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. csbfv12gALT 5536 is csbfv12gALTVD 28675 without virtual deductions and was automatically derived from csbfv12gALTVD 28675.
1::  |-  (. A  e.  C  ->.  A  e.  C ).
2:1:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y }  =  {  y } ).
3:1:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " { B  } )  =  ( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } ) ).
4:1:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { B }  =  {  [_ A  /  x ]_ B } ).
5:4:  |-  (. A  e.  C  ->.  ( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } )  =  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ).
6:3,5:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " { B  } )  =  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ).
7:1:  |-  (. A  e.  C  ->.  ( [. A  /  x ]. ( F " {  B } )  =  { y }  <->  [_ A  /  x ]_ ( F " { B } )  =  [_ A  /  x ]_ { y } ) ).
8:6,2:  |-  (. A  e.  C  ->.  ( [_ A  /  x ]_ ( F " {  B } )  =  [_ A  /  x ]_ { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
9:7,8:  |-  (. A  e.  C  ->.  ( [. A  /  x ]. ( F " {  B } )  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } )  ).
10:9:  |-  (. A  e.  C  ->.  A. y ( [. A  /  x ]. ( F  " { B } )  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
11:10:  |-  (. A  e.  C  ->.  { y  |  [. A  /  x ]. ( F  " { B } )  =  { y } }  =  { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } } ).
12:1:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y  |  ( F  " { B } )  =  { y } }  =  { y  |  [. A  /  x ]. ( F " { B } )  =  { y } } ).
13:11,12:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y  |  ( F  " { B } )  =  { y } }  =  { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y  } } ).
14:13:  |-  (. A  e.  C  ->.  U. [_ A  /  x ]_ { y  |  (  F " { B } )  =  { y } }  =  U. { y  |  ( [_ A  /  x ]_ F "  { [_ A  /  x ]_ B } )  =  { y } } ).
15:1:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ U. { y  |  (  F " { B } )  =  { y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  { y } } ).
16:14,15:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ U. { y  |  (  F " { B } )  =  { y } }  =  U. { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } } ).
17::  |-  ( F `  B )  =  U. { y  |  ( F " { B } )  =  { y } }
18:17:  |-  A. x ( F `  B )  =  U. { y  |  ( F " { B  } )  =  { y } }
19:1,18:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B )  =  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  { y } } ).
20:16,19:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B )  =  U. { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } } ).
21::  |-  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B )  =  U. { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }
22:20,21:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B )  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) ).
qed:22:  |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F `  B )  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbfv12gALTVD  |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F `
 B )  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) )

Proof of Theorem csbfv12gALTVD
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 idn1 28342 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  A  e.  C ).
2 sbceqg 3097 . . . . . . . . . . 11  |-  ( A  e.  C  ->  ( [. A  /  x ]. ( F " { B } )  =  {
y }  <->  [_ A  /  x ]_ ( F " { B } )  = 
[_ A  /  x ]_ { y } ) )
31, 2e1_ 28399 . . . . . . . . . 10  |-  (. A  e.  C  ->.  ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  [_ A  /  x ]_ ( F " { B } )  =  [_ A  /  x ]_ {
y } ) ).
4 csbima12g 5022 . . . . . . . . . . . . 13  |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F
" { B }
)  =  ( [_ A  /  x ]_ F "
[_ A  /  x ]_ { B } ) )
51, 4e1_ 28399 . . . . . . . . . . . 12  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " { B } )  =  (
[_ A  /  x ]_ F " [_ A  /  x ]_ { B } ) ).
6 csbsng 3692 . . . . . . . . . . . . . 14  |-  ( A  e.  C  ->  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }
)
71, 6e1_ 28399 . . . . . . . . . . . . 13  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B } ).
8 imaeq2 5008 . . . . . . . . . . . . 13  |-  ( [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) )
97, 8e1_ 28399 . . . . . . . . . . . 12  |-  (. A  e.  C  ->.  ( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } )  =  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ).
10 eqeq1 2289 . . . . . . . . . . . . 13  |-  ( [_ A  /  x ]_ ( F " { B }
)  =  ( [_ A  /  x ]_ F "
[_ A  /  x ]_ { B } )  ->  ( [_ A  /  x ]_ ( F
" { B }
)  =  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  <-> 
( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ) )
1110biimprd 214 . . . . . . . . . . . 12  |-  ( [_ A  /  x ]_ ( F " { B }
)  =  ( [_ A  /  x ]_ F "
[_ A  /  x ]_ { B } )  ->  ( ( [_ A  /  x ]_ F "
[_ A  /  x ]_ { B } )  =  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  ->  [_ A  /  x ]_ ( F " { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ) )
125, 9, 11e11 28460 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ).
13 csbconstg 3095 . . . . . . . . . . . 12  |-  ( A  e.  C  ->  [_ A  /  x ]_ { y }  =  { y } )
141, 13e1_ 28399 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y }  =  { y } ).
15 eqeq12 2295 . . . . . . . . . . . 12  |-  ( (
[_ A  /  x ]_ ( F " { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  /\  [_ A  /  x ]_ { y }  =  { y } )  ->  ( [_ A  /  x ]_ ( F " { B } )  =  [_ A  /  x ]_ {
y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) )
1615ex 423 . . . . . . . . . . 11  |-  ( [_ A  /  x ]_ ( F " { B }
)  =  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  ->  ( [_ A  /  x ]_ { y }  =  { y }  ->  ( [_ A  /  x ]_ ( F " { B }
)  =  [_ A  /  x ]_ { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ) )
1712, 14, 16e11 28460 . . . . . . . . . 10  |-  (. A  e.  C  ->.  ( [_ A  /  x ]_ ( F
" { B }
)  =  [_ A  /  x ]_ { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
18 bibi1 317 . . . . . . . . . . 11  |-  ( (
[. A  /  x ]. ( F " { B } )  =  {
y }  <->  [_ A  /  x ]_ ( F " { B } )  = 
[_ A  /  x ]_ { y } )  ->  ( ( [. A  /  x ]. ( F " { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } )  <-> 
( [_ A  /  x ]_ ( F " { B } )  =  [_ A  /  x ]_ {
y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ) )
1918biimprd 214 . . . . . . . . . 10  |-  ( (
[. A  /  x ]. ( F " { B } )  =  {
y }  <->  [_ A  /  x ]_ ( F " { B } )  = 
[_ A  /  x ]_ { y } )  ->  ( ( [_ A  /  x ]_ ( F " { B }
)  =  [_ A  /  x ]_ { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } )  ->  ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ) )
203, 17, 19e11 28460 . . . . . . . . 9  |-  (. A  e.  C  ->.  ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
2120gen11 28388 . . . . . . . 8  |-  (. A  e.  C  ->.  A. y ( [. A  /  x ]. ( F " { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
22 abbi 2393 . . . . . . . . 9  |-  ( A. y ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } )  <->  { y  |  [. A  /  x ]. ( F " { B }
)  =  { y } }  =  {
y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } } )
2322biimpi 186 . . . . . . . 8  |-  ( A. y ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } )  ->  { y  | 
[. A  /  x ]. ( F " { B } )  =  {
y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } )
2421, 23e1_ 28399 . . . . . . 7  |-  (. A  e.  C  ->.  { y  | 
[. A  /  x ]. ( F " { B } )  =  {
y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
25 csbabg 3142 . . . . . . . 8  |-  ( A  e.  C  ->  [_ A  /  x ]_ { y  |  ( F " { B } )  =  { y } }  =  { y  |  [. A  /  x ]. ( F " { B }
)  =  { y } } )
261, 25e1_ 28399 . . . . . . 7  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  { y  |  [. A  /  x ]. ( F " { B }
)  =  { y } } ).
27 eqeq2 2292 . . . . . . . 8  |-  ( { y  |  [. A  /  x ]. ( F
" { B }
)  =  { y } }  =  {
y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }  ->  ( [_ A  /  x ]_ {
y  |  ( F
" { B }
)  =  { y } }  =  {
y  |  [. A  /  x ]. ( F
" { B }
)  =  { y } }  <->  [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ) )
2827biimpd 198 . . . . . . 7  |-  ( { y  |  [. A  /  x ]. ( F
" { B }
)  =  { y } }  =  {
y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }  ->  ( [_ A  /  x ]_ {
y  |  ( F
" { B }
)  =  { y } }  =  {
y  |  [. A  /  x ]. ( F
" { B }
)  =  { y } }  ->  [_ A  /  x ]_ { y  |  ( F " { B } )  =  { y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ) )
2924, 26, 28e11 28460 . . . . . 6  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
30 unieq 3836 . . . . . 6  |-  ( [_ A  /  x ]_ {
y  |  ( F
" { B }
)  =  { y } }  =  {
y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }  ->  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  { y } }  =  U. { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }
)
3129, 30e1_ 28399 . . . . 5  |-  (. A  e.  C  ->.  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
32 csbunig 3835 . . . . . 6  |-  ( A  e.  C  ->  [_ A  /  x ]_ U. {
y  |  ( F
" { B }
)  =  { y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } } )
331, 32e1_ 28399 . . . . 5  |-  (. A  e.  C  ->.  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } } ).
34 eqeq2 2292 . . . . . 6  |-  ( U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } }  ->  (
[_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  <->  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  { y } }  =  U. { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }
) )
3534biimpd 198 . . . . 5  |-  ( U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } }  ->  (
[_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  ->  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ) )
3631, 33, 35e11 28460 . . . 4  |-  (. A  e.  C  ->.  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
37 dffv4 5522 . . . . . 6  |-  ( F `
 B )  = 
U. { y  |  ( F " { B } )  =  {
y } }
3837ax-gen 1533 . . . . 5  |-  A. x
( F `  B
)  =  U. {
y  |  ( F
" { B }
)  =  { y } }
39 csbeq2g 28315 . . . . 5  |-  ( A  e.  C  ->  ( A. x ( F `  B )  =  U. { y  |  ( F " { B } )  =  {
y } }  ->  [_ A  /  x ]_ ( F `  B )  =  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  { y } }
) )
401, 38, 39e10 28467 . . . 4  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  [_ A  /  x ]_ U. {
y  |  ( F
" { B }
)  =  { y } } ).
41 eqeq2 2292 . . . . 5  |-  ( [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } }  ->  (
[_ A  /  x ]_ ( F `  B
)  =  [_ A  /  x ]_ U. {
y  |  ( F
" { B }
)  =  { y } }  <->  [_ A  /  x ]_ ( F `  B )  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ) )
4241biimpd 198 . . . 4  |-  ( [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } }  ->  (
[_ A  /  x ]_ ( F `  B
)  =  [_ A  /  x ]_ U. {
y  |  ( F
" { B }
)  =  { y } }  ->  [_ A  /  x ]_ ( F `
 B )  = 
U. { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }
) )
4336, 40, 42e11 28460 . . 3  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  U. {
y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } } ).
44 dffv4 5522 . . 3  |-  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B )  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } }
45 eqeq2 2292 . . . 4  |-  ( (
[_ A  /  x ]_ F `  [_ A  /  x ]_ B )  =  U. { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }  ->  ( [_ A  /  x ]_ ( F `  B )  =  (
[_ A  /  x ]_ F `  [_ A  /  x ]_ B )  <->  [_ A  /  x ]_ ( F `  B
)  =  U. {
y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } } ) )
4645biimprcd 216 . . 3  |-  ( [_ A  /  x ]_ ( F `  B )  =  U. { y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } }  ->  ( ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B )  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } }  ->  [_ A  /  x ]_ ( F `  B )  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) ) )
4743, 44, 46e10 28467 . 2  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) ).
4847in1 28339 1  |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F `
 B )  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527    = wceq 1623    e. wcel 1684   {cab 2269   [.wsbc 2991   [_csb 3081   {csn 3640   U.cuni 3827   "cima 4692   ` cfv 5255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-xp 4695  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fv 5263  df-vd1 28338
  Copyright terms: Public domain W3C validator