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

Theorem csbfv12gALTVD 37296
Description: Virtual deduction proof of csbfv12gALTOLD 37213. 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 37213 is csbfv12gALTVD 37296 without virtual deductions and was automatically derived from csbfv12gALTVD 37296.
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 36944 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  A  e.  C ).
2 sbceqg 3773 . . . . . . . . . . 11  |-  ( A  e.  C  ->  ( [. A  /  x ]. ( F " { B } )  =  {
y }  <->  [_ A  /  x ]_ ( F " { B } )  = 
[_ A  /  x ]_ { y } ) )
31, 2e1a 37006 . . . . . . . . . 10  |-  (. A  e.  C  ->.  ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  [_ A  /  x ]_ ( F " { B } )  =  [_ A  /  x ]_ {
y } ) ).
4 csbima12gOLD 5186 . . . . . . . . . . . . 13  |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F
" { B }
)  =  ( [_ A  /  x ]_ F "
[_ A  /  x ]_ { B } ) )
51, 4e1a 37006 . . . . . . . . . . . 12  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " { B } )  =  (
[_ A  /  x ]_ F " [_ A  /  x ]_ { B } ) ).
6 csbsng 4030 . . . . . . . . . . . . . 14  |-  ( A  e.  C  ->  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }
)
71, 6e1a 37006 . . . . . . . . . . . . 13  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B } ).
8 imaeq2 5164 . . . . . . . . . . . . 13  |-  ( [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) )
97, 8e1a 37006 . . . . . . . . . . . 12  |-  (. A  e.  C  ->.  ( [_ A  /  x ]_ F " [_ A  /  x ]_ { B } )  =  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ).
10 eqeq1 2455 . . . . . . . . . . . . 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 227 . . . . . . . . . . . 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 37067 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " { B } )  =  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } ) ).
13 csbconstg 3376 . . . . . . . . . . . 12  |-  ( A  e.  C  ->  [_ A  /  x ]_ { y }  =  { y } )
141, 13e1a 37006 . . . . . . . . . . 11  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y }  =  { y } ).
15 eqeq12 2464 . . . . . . . . . . . 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 436 . . . . . . . . . . 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 37067 . . . . . . . . . 10  |-  (. A  e.  C  ->.  ( [_ A  /  x ]_ ( F
" { B }
)  =  [_ A  /  x ]_ { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
18 bibi1 329 . . . . . . . . . . 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 227 . . . . . . . . . 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 37067 . . . . . . . . 9  |-  (. A  e.  C  ->.  ( [. A  /  x ]. ( F
" { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
2120gen11 36995 . . . . . . . 8  |-  (. A  e.  C  ->.  A. y ( [. A  /  x ]. ( F " { B }
)  =  { y }  <->  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } ) ).
22 abbi 2565 . . . . . . . . 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 198 . . . . . . . 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 37006 . . . . . . 7  |-  (. A  e.  C  ->.  { y  | 
[. A  /  x ]. ( F " { B } )  =  {
y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
25 csbabgOLD 37211 . . . . . . . 8  |-  ( A  e.  C  ->  [_ A  /  x ]_ { y  |  ( F " { B } )  =  { y } }  =  { y  |  [. A  /  x ]. ( F " { B }
)  =  { y } } )
261, 25e1a 37006 . . . . . . 7  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  { y  |  [. A  /  x ]. ( F " { B }
)  =  { y } } ).
27 eqeq2 2462 . . . . . . . 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 211 . . . . . . 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 37067 . . . . . 6  |-  (. A  e.  C  ->.  [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
30 unieq 4206 . . . . . 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 37006 . . . . 5  |-  (. A  e.  C  ->.  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
32 csbunigOLD 37212 . . . . . 6  |-  ( A  e.  C  ->  [_ A  /  x ]_ U. {
y  |  ( F
" { B }
)  =  { y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } } )
331, 32e1a 37006 . . . . 5  |-  (. A  e.  C  ->.  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. [_ A  /  x ]_ { y  |  ( F " { B } )  =  {
y } } ).
34 eqeq2 2462 . . . . . 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 211 . . . . 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 37067 . . . 4  |-  (. A  e.  C  ->.  [_ A  /  x ]_ U. { y  |  ( F " { B } )  =  {
y } }  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } } ).
37 dffv4 5862 . . . . . 6  |-  ( F `
 B )  = 
U. { y  |  ( F " { B } )  =  {
y } }
3837ax-gen 1669 . . . . 5  |-  A. x
( F `  B
)  =  U. {
y  |  ( F
" { B }
)  =  { y } }
39 csbeq2gOLD 36916 . . . . 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 37073 . . . 4  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  [_ A  /  x ]_ U. {
y  |  ( F
" { B }
)  =  { y } } ).
41 eqeq2 2462 . . . . 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 211 . . . 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 37067 . . 3  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  U. {
y  |  ( [_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  { y } } ).
44 dffv4 5862 . . 3  |-  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B )  =  U. { y  |  (
[_ A  /  x ]_ F " { [_ A  /  x ]_ B } )  =  {
y } }
45 eqeq2 2462 . . . 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 229 . . 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 37073 . 2  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F `  B
)  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) ).
4847in1 36941 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 188   A.wal 1442    = wceq 1444    e. wcel 1887   {cab 2437   [.wsbc 3267   [_csb 3363   {csn 3968   U.cuni 4198   "cima 4837   ` cfv 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-xp 4840  df-cnv 4842  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fv 5590  df-vd1 36940
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator