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

Theorem csbrngVD 37160
Description: Virtual deduction proof of csbrngOLD 37084. 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. csbrngOLD 37084 is csbrngVD 37160 without virtual deductions and was automatically derived from csbrngVD 37160.
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 36809 . . . . . . . . . . . 12  |-  (. A  e.  V  ->.  A  e.  V ).
2 sbcel12gOLD 36769 . . . . . . . . . . . 12  |-  ( A  e.  V  ->  ( [. A  /  x ]. <. w ,  y
>.  e.  B  <->  [_ A  /  x ]_ <. w ,  y
>.  e.  [_ A  /  x ]_ B ) )
31, 2e1a 36871 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( [. A  /  x ]. <. w ,  y >.  e.  B  <->  [_ A  /  x ]_ <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
4 csbconstg 3409 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  [_ A  /  x ]_ <. w ,  y >.  =  <. w ,  y >. )
51, 4e1a 36871 . . . . . . . . . . . 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, 6e1a 36871 . . . . . . . . . . 11  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ <. w ,  y >.  e.  [_ A  /  x ]_ B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B ) ).
8 bibi1 329 . . . . . . . . . . . 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 227 . . . . . . . . . . 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 36932 . . . . . . . . . 10  |-  (. A  e.  V  ->.  ( [. A  /  x ]. <. w ,  y >.  e.  B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B ) ).
1110gen11 36860 . . . . . . . . 9  |-  (. A  e.  V  ->.  A. w ( [. A  /  x ]. <. w ,  y >.  e.  B  <->  <.
w ,  y >.  e.  [_ A  /  x ]_ B ) ).
12 exbi 1712 . . . . . . . . 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, 12e1a 36871 . . . . . . . 8  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
14 sbcexgOLD 36768 . . . . . . . . . 10  |-  ( A  e.  V  ->  ( [. A  /  x ]. E. w <. w ,  y >.  e.  B  <->  E. w [. A  /  x ]. <. w ,  y
>.  e.  B ) )
1514bicomd 205 . . . . . . . . 9  |-  ( A  e.  V  ->  ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  [. A  /  x ]. E. w <. w ,  y >.  e.  B
) )
161, 15e1a 36871 . . . . . . . 8  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. <. w ,  y
>.  e.  B  <->  [. A  /  x ]. E. w <. w ,  y >.  e.  B
) ).
17 bitr3 36731 . . . . . . . . 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 33 . . . . . . . 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 36932 . . . . . . 7  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w <. w ,  y >.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B
) ).
2019gen11 36860 . . . . . 6  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. E. w <. w ,  y
>.  e.  B  <->  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B ) ).
21 abbi 2554 . . . . . . 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 198 . . . . . 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, 22e1a 36871 . . . . 5  |-  (. A  e.  V  ->.  { y  | 
[. A  /  x ]. E. w <. w ,  y >.  e.  B }  =  { y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ).
24 csbabgOLD 37078 . . . . . 6  |-  ( A  e.  V  ->  [_ A  /  x ]_ { y  |  E. w <. w ,  y >.  e.  B }  =  { y  |  [. A  /  x ]. E. w <. w ,  y >.  e.  B } )
251, 24e1a 36871 . . . . 5  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { y  |  E. w <. w ,  y
>.  e.  B }  =  { y  |  [. A  /  x ]. E. w <. w ,  y
>.  e.  B } ).
26 eqeq2 2438 . . . . . 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 211 . . . . 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 36932 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { y  |  E. w <. w ,  y
>.  e.  B }  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B } ).
29 dfrn3 5041 . . . . . 6  |-  ran  B  =  { y  |  E. w <. w ,  y
>.  e.  B }
3029ax-gen 1666 . . . . 5  |-  A. x ran  B  =  { y  |  E. w <. w ,  y >.  e.  B }
31 csbeq2gOLD 36780 . . . . 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 36938 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  [_ A  /  x ]_ {
y  |  E. w <. w ,  y >.  e.  B } ).
33 eqeq2 2438 . . . . 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 211 . . . 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 36932 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  {
y  |  E. w <. w ,  y >.  e.  [_ A  /  x ]_ B } ).
36 dfrn3 5041 . . 3  |-  ran  [_ A  /  x ]_ B  =  { y  |  E. w <. w ,  y
>.  e.  [_ A  /  x ]_ B }
37 eqeq2 2438 . . . 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 229 . . 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 36938 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ran  B  =  ran  [_ A  /  x ]_ B ).
4039in1 36806 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ ran  B  =  ran  [_ A  /  x ]_ B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   A.wal 1436    = wceq 1438   E.wex 1660    e. wcel 1869   {cab 2408   [.wsbc 3300   [_csb 3396   <.cop 4003   ran crn 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-cnv 4859  df-dm 4861  df-rn 4862  df-vd1 36805
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator