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

Theorem csbrngVD 28945
Description: Virtual deduction proof of csbrng 5106. 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. csbrng 5106 is csbrngVD 28945 without virtual deductions and was automatically derived from csbrngVD 28945.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. <. w ,. y >.  e.  B  <->  [_ A  /  x ]_ <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
3:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ <. w ,. y >.  =  <. w ,  y >. ).
4:3:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ <. w ,. y >.  e.  [_ A  /  x ]_ B  <->  <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
5:2,4:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. <. w ,. y >.  e.  B  <->  <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
6:5:  |-  (. A  e.  V  ->.  A. w ( [. A  /  x ]. <. w ,.  y >.  e.  B  <->  <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
7:6:  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. <. w ,.  y >.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
8:1:  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. <. w ,.  y >.  e.  B  <->  [. A  /  x ]. E. w <. w ,  y >.  e.  B ) ).
9:7,8:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w <. w  ,. y >.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
10:9:  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. E. w  <. w ,  y >.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
11:10:  |-  (. A  e.  V  ->.  { y  |  [. A  /  x ]. E. w <.  w ,  y >.  e.  B }  =  { y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ).
12:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { y  |  E. w  <. w ,  y >.  e.  B }  =  { y  |  [. A  /  x ]. E. w <. w ,  y >.  e.  B } ).
13:11,12:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { y  |  E. w  <. w ,  y >.  e.  B }  =  { y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ).
14::  |-  ran  B  =  { y  |  E. w <. w ,. y >.  e.  B }
15:14:  |-  A. x ran  B  =  { y  |  E. w <. w ,. y >.  e.  B }
16:1,15:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  [_ A  /  x ]_ { y  |  E. w <. w ,  y >.  e.  B } ).
17:13,16:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  { y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ).
18::  |-  ran  [_ A  /  x ]_ B  =  { y  |  E. w <. w  ,. y >.  e.  [_ A  /  x ]_ B }
19:17,18:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  ran  [_  A  /  x ]_ B ).
qed:19:  |-  ( A  e.  V  ->  [_ A  /  x ]_ ran  B  =  ran  [_ A  /  x ]_ B )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbrngVD  |-  ( A  e.  V  ->  [_ A  /  x ]_ ran  B  =  ran  [_ A  /  x ]_ B )

Proof of Theorem csbrngVD
Dummy variables  w  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 28602 . . . . . . . . . . . 12  |-  (. A  e.  V  ->.  A  e.  V ).
2 sbcel12g 3258 . . . . . . . . . . . 12  |-  ( A  e.  V  ->  ( [. A  /  x ]. <. w ,  y
>.  e.  B  <->  [_ A  /  x ]_ <. w ,  y
>.  e.  [_ A  /  x ]_ B ) )
31, 2e1_ 28665 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( [. A  /  x ]. <. w ,  y >.  e.  B  <->  [_ A  /  x ]_ <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
4 csbconstg 3257 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  [_ A  /  x ]_ <. w ,  y >.  =  <. w ,  y >. )
51, 4e1_ 28665 . . . . . . . . . . . 12  |-  (. A  e.  V  ->.  [_ A  /  x ]_ <. w ,  y
>.  =  <. w ,  y >. ).
6 eleq1 2495 . . . . . . . . . . . 12  |-  ( [_ A  /  x ]_ <. w ,  y >.  =  <. w ,  y >.  ->  ( [_ A  /  x ]_ <. w ,  y
>.  e.  [_ A  /  x ]_ B  <->  <. w ,  y >.  e.  [_ A  /  x ]_ B ) )
75, 6e1_ 28665 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ <. w ,  y >.  e.  [_ A  /  x ]_ B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B ) ).
8 bibi1 318 . . . . . . . . . . . 12  |-  ( (
[. A  /  x ]. <. w ,  y
>.  e.  B  <->  [_ A  /  x ]_ <. w ,  y
>.  e.  [_ A  /  x ]_ B )  -> 
( ( [. A  /  x ]. <. w ,  y >.  e.  B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B )  <->  ( [_ A  /  x ]_ <. w ,  y >.  e.  [_ A  /  x ]_ B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B ) ) )
98biimprd 215 . . . . . . . . . . 11  |-  ( (
[. A  /  x ]. <. w ,  y
>.  e.  B  <->  [_ A  /  x ]_ <. w ,  y
>.  e.  [_ A  /  x ]_ B )  -> 
( ( [_ A  /  x ]_ <. w ,  y >.  e.  [_ A  /  x ]_ B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B )  ->  ( [. A  /  x ]. <. w ,  y
>.  e.  B  <->  <. w ,  y >.  e.  [_ A  /  x ]_ B ) ) )
103, 7, 9e11 28726 . . . . . . . . . 10  |-  (. A  e.  V  ->.  ( [. A  /  x ]. <. w ,  y >.  e.  B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B ) ).
1110gen11 28654 . . . . . . . . 9  |-  (. A  e.  V  ->.  A. w ( [. A  /  x ]. <. w ,  y >.  e.  B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B ) ).
12 exbi 1591 . . . . . . . . 9  |-  ( A. w ( [. A  /  x ]. <. w ,  y >.  e.  B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B )  ->  ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) )
1311, 12e1_ 28665 . . . . . . . 8  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
14 sbcexg 3203 . . . . . . . . . 10  |-  ( A  e.  V  ->  ( [. A  /  x ]. E. w <. w ,  y >.  e.  B  <->  E. w [. A  /  x ]. <. w ,  y
>.  e.  B ) )
1514bicomd 193 . . . . . . . . 9  |-  ( A  e.  V  ->  ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  [. A  /  x ]. E. w <. w ,  y >.  e.  B
) )
161, 15e1_ 28665 . . . . . . . 8  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  [. A  /  x ]. E. w <. w ,  y >.  e.  B
) ).
17 bitr3 28530 . . . . . . . . 9  |-  ( ( E. w [. A  /  x ]. <. w ,  y >.  e.  B  <->  [. A  /  x ]. E. w <. w ,  y
>.  e.  B )  -> 
( ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B )  ->  ( [. A  /  x ]. E. w <. w ,  y >.  e.  B  <->  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B ) ) )
1817com12 29 . . . . . . . 8  |-  ( ( E. w [. A  /  x ]. <. w ,  y >.  e.  B  <->  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B )  -> 
( ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  [. A  /  x ]. E. w <. w ,  y >.  e.  B
)  ->  ( [. A  /  x ]. E. w <. w ,  y
>.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) ) )
1913, 16, 18e11 28726 . . . . . . 7  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w <. w ,  y >.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B
) ).
2019gen11 28654 . . . . . 6  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. E. w <. w ,  y
>.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
21 abbi 2545 . . . . . . 7  |-  ( A. y ( [. A  /  x ]. E. w <. w ,  y >.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B
)  <->  { y  |  [. A  /  x ]. E. w <. w ,  y
>.  e.  B }  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B } )
2221biimpi 187 . . . . . 6  |-  ( A. y ( [. A  /  x ]. E. w <. w ,  y >.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B
)  ->  { y  |  [. A  /  x ]. E. w <. w ,  y >.  e.  B }  =  { y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } )
2320, 22e1_ 28665 . . . . 5  |-  (. A  e.  V  ->.  { y  | 
[. A  /  x ]. E. w <. w ,  y >.  e.  B }  =  { y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ).
24 csbabg 3302 . . . . . 6  |-  ( A  e.  V  ->  [_ A  /  x ]_ { y  |  E. w <. w ,  y >.  e.  B }  =  { y  |  [. A  /  x ]. E. w <. w ,  y >.  e.  B } )
251, 24e1_ 28665 . . . . 5  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { y  |  E. w <. w ,  y
>.  e.  B }  =  { y  |  [. A  /  x ]. E. w <. w ,  y
>.  e.  B } ).
26 eqeq2 2444 . . . . . 6  |-  ( { y  |  [. A  /  x ]. E. w <. w ,  y >.  e.  B }  =  {
y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ { y  |  E. w <. w ,  y
>.  e.  B }  =  { y  |  [. A  /  x ]. E. w <. w ,  y
>.  e.  B }  <->  [_ A  /  x ]_ { y  |  E. w <. w ,  y >.  e.  B }  =  { y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ) )
2726biimpd 199 . . . . 5  |-  ( { y  |  [. A  /  x ]. E. w <. w ,  y >.  e.  B }  =  {
y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ { y  |  E. w <. w ,  y
>.  e.  B }  =  { y  |  [. A  /  x ]. E. w <. w ,  y
>.  e.  B }  ->  [_ A  /  x ]_ { y  |  E. w <. w ,  y
>.  e.  B }  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B } ) )
2823, 25, 27e11 28726 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { y  |  E. w <. w ,  y
>.  e.  B }  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B } ).
29 dfrn3 5052 . . . . . 6  |-  ran  B  =  { y  |  E. w <. w ,  y
>.  e.  B }
3029ax-gen 1555 . . . . 5  |-  A. x ran  B  =  { y  |  E. w <. w ,  y >.  e.  B }
31 csbeq2g 28573 . . . . 5  |-  ( A  e.  V  ->  ( A. x ran  B  =  { y  |  E. w <. w ,  y
>.  e.  B }  ->  [_ A  /  x ]_ ran  B  =  [_ A  /  x ]_ { y  |  E. w <. w ,  y >.  e.  B } ) )
321, 30, 31e10 28732 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  [_ A  /  x ]_ {
y  |  E. w <. w ,  y >.  e.  B } ).
33 eqeq2 2444 . . . . 5  |-  ( [_ A  /  x ]_ {
y  |  E. w <. w ,  y >.  e.  B }  =  {
y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ ran  B  =  [_ A  /  x ]_ {
y  |  E. w <. w ,  y >.  e.  B }  <->  [_ A  /  x ]_ ran  B  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B } ) )
3433biimpd 199 . . . 4  |-  ( [_ A  /  x ]_ {
y  |  E. w <. w ,  y >.  e.  B }  =  {
y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ ran  B  =  [_ A  /  x ]_ {
y  |  E. w <. w ,  y >.  e.  B }  ->  [_ A  /  x ]_ ran  B  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B } ) )
3528, 32, 34e11 28726 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  {
y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ).
36 dfrn3 5052 . . 3  |-  ran  [_ A  /  x ]_ B  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B }
37 eqeq2 2444 . . . 4  |-  ( ran  [_ A  /  x ]_ B  =  {
y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ ran  B  =  ran  [_ A  /  x ]_ B 
<-> 
[_ A  /  x ]_ ran  B  =  {
y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ) )
3837biimprcd 217 . . 3  |-  ( [_ A  /  x ]_ ran  B  =  { y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B }  ->  ( ran  [_ A  /  x ]_ B  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B }  ->  [_ A  /  x ]_ ran  B  =  ran  [_ A  /  x ]_ B ) )
3935, 36, 38e10 28732 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  ran  [_ A  /  x ]_ B ).
4039in1 28599 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ ran  B  =  ran  [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725   {cab 2421   [.wsbc 3153   [_csb 3243   <.cop 3809   ran crn 4871
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-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-cnv 4878  df-dm 4880  df-rn 4881  df-vd1 28598
  Copyright terms: Public domain W3C validator