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

Theorem csbfv12gALTVD 37156
Description: Virtual deduction proof of csbfv12gALTOLD 37073. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbfv12gALTOLD 37073 is csbfv12gALTVD 37156 without virtual deductions and was automatically derived from csbfv12gALTVD 37156.
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 36802 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  A  e.  C ).
2 sbceqg 3801 . . . . . . . . . . 11  |-  ( A  e.  C  ->  ( [. A  /  x ]. ( F " { B } )  =  {
y }  <->  [_ A  /  x ]_ ( F " { B } )  = 
[_ A  /  x ]_ { y } ) )
31, 2e1a 36864 . . . . . . . . . 10  |-  (. A  e.  C  ->.  ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  [_ A  /  x ]_ ( F " { B } )  =  [_ A  /  x ]_ {
y } ) ).
4 csbima12gOLD 5201 . . . . . . . . . . . . 13  |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F
" { B }
)  =  ( [_ A  /  x ]_ F "
[_ A  /  x ]_ { B } ) )
51, 4e1a 36864 . . . . . . . . . . . 12  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " { B } )  =  (
[_ A  /  x ]_ F " [_ A  /  x ]_ { B } ) ).
6 csbsng 4055 . . . . . . . . . . . . . 14  |-  ( A  e.  C  ->  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }
)
71, 6e1a 36864 . . . . . . . . . . . . 13  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B } ).
8 imaeq2 5179 . . . . . . . . . . . . 13  |-  ( [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) )
97, 8e1a 36864 . . . . . . . . . . . 12  |-  (. A  e.  C  ->.  ( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } )  =  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ).
10 eqeq1 2426 . . . . . . . . . . . . 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 226 . . . . . . . . . . . 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 36925 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ).
13 csbconstg 3408 . . . . . . . . . . . 12  |-  ( A  e.  C  ->  [_ A  /  x ]_ { y }  =  { y } )
141, 13e1a 36864 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y }  =  { y } ).
15 eqeq12 2441 . . . . . . . . . . . 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 435 . . . . . . . . . . 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 36925 . . . . . . . . . 10  |-  (. A  e.  C  ->.  ( [_ A  /  x ]_ ( F
" { B }
)  =  [_ A  /  x ]_ { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
18 bibi1 328 . . . . . . . . . . 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 226 . . . . . . . . . 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 36925 . . . . . . . . 9  |-  (. A  e.  C  ->.  ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
2120gen11 36853 . . . . . . . 8  |-  (. A  e.  C  ->.  A. y ( [. A  /  x ]. ( F " { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
22 abbi 2553 . . . . . . . . 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 197 . . . . . . . 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, 23e1a 36864 . . . . . . 7  |-  (. A  e.  C  ->.  { y  | 
[. A  /  x ]. ( F " { B } )  =  {
y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
25 csbabgOLD 37071 . . . . . . . 8  |-  ( A  e.  C  ->  [_ A  /  x ]_ { y  |  ( F " { B } )  =  { y } }  =  { y  |  [. A  /  x ]. ( F " { B }
)  =  { y } } )
261, 25e1a 36864 . . . . . . 7  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  { y  |  [. A  /  x ]. ( F " { B }
)  =  { y } } ).
27 eqeq2 2437 . . . . . . . 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 210 . . . . . . 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 36925 . . . . . 6  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
30 unieq 4224 . . . . . 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, 30e1a 36864 . . . . 5  |-  (. A  e.  C  ->.  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
32 csbunigOLD 37072 . . . . . 6  |-  ( A  e.  C  ->  [_ A  /  x ]_ U. {
y  |  ( F
" { B }
)  =  { y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } } )
331, 32e1a 36864 . . . . 5  |-  (. A  e.  C  ->.  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } } ).
34 eqeq2 2437 . . . . . 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 210 . . . . 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 36925 . . . 4  |-  (. A  e.  C  ->.  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
37 dffv4 5874 . . . . . 6  |-  ( F `
 B )  = 
U. { y  |  ( F " { B } )  =  {
y } }
3837ax-gen 1665 . . . . 5  |-  A. x
( F `  B
)  =  U. {
y  |  ( F
" { B }
)  =  { y } }
39 csbeq2gOLD 36773 . . . . 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 36931 . . . 4  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  [_ A  /  x ]_ U. {
y  |  ( F
" { B }
)  =  { y } } ).
41 eqeq2 2437 . . . . 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 210 . . . 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 36925 . . 3  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  U. {
y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } } ).
44 dffv4 5874 . . 3  |-  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B )  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } }
45 eqeq2 2437 . . . 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 228 . . 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 36931 . 2  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) ).
4847in1 36799 1  |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F `
 B )  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435    = wceq 1437    e. wcel 1868   {cab 2407   [.wsbc 3299   [_csb 3395   {csn 3996   U.cuni 4216   "cima 4852   ` cfv 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-xp 4855  df-cnv 4857  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fv 5605  df-vd1 36798
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator