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

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

Proof of Theorem csbsngVD
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 idn1 28592 . . . . . . . . 9  |-  (. A  e.  V  ->.  A  e.  V ).
2 sbceqg 3259 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  =  B  <->  [_ A  /  x ]_ y  =  [_ A  /  x ]_ B ) )
31, 2e1_ 28655 . . . . . . . 8  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  =  B  <->  [_ A  /  x ]_ y  =  [_ A  /  x ]_ B ) ).
4 csbconstg 3257 . . . . . . . . . 10  |-  ( A  e.  V  ->  [_ A  /  x ]_ y  =  y )
51, 4e1_ 28655 . . . . . . . . 9  |-  (. A  e.  V  ->.  [_ A  /  x ]_ y  =  y ).
6 eqeq1 2441 . . . . . . . . 9  |-  ( [_ A  /  x ]_ y  =  y  ->  ( [_ A  /  x ]_ y  =  [_ A  /  x ]_ B  <->  y  =  [_ A  /  x ]_ B
) )
75, 6e1_ 28655 . . . . . . . 8  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ y  = 
[_ A  /  x ]_ B  <->  y  =  [_ A  /  x ]_ B
) ).
8 bibi1 318 . . . . . . . . 9  |-  ( (
[. A  /  x ]. y  =  B  <->  [_ A  /  x ]_ y  =  [_ A  /  x ]_ B )  -> 
( ( [. A  /  x ]. y  =  B  <->  y  =  [_ A  /  x ]_ B
)  <->  ( [_ A  /  x ]_ y  = 
[_ A  /  x ]_ B  <->  y  =  [_ A  /  x ]_ B
) ) )
98biimprd 215 . . . . . . . 8  |-  ( (
[. A  /  x ]. y  =  B  <->  [_ A  /  x ]_ y  =  [_ A  /  x ]_ B )  -> 
( ( [_ A  /  x ]_ y  = 
[_ A  /  x ]_ B  <->  y  =  [_ A  /  x ]_ B
)  ->  ( [. A  /  x ]. y  =  B  <->  y  =  [_ A  /  x ]_ B
) ) )
103, 7, 9e11 28716 . . . . . . 7  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  =  B  <->  y  =  [_ A  /  x ]_ B
) ).
1110gen11 28644 . . . . . 6  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. y  =  B  <->  y  =  [_ A  /  x ]_ B
) ).
12 abbi 2545 . . . . . . 7  |-  ( A. y ( [. A  /  x ]. y  =  B  <->  y  =  [_ A  /  x ]_ B
)  <->  { y  |  [. A  /  x ]. y  =  B }  =  {
y  |  y  = 
[_ A  /  x ]_ B } )
1312biimpi 187 . . . . . 6  |-  ( A. y ( [. A  /  x ]. y  =  B  <->  y  =  [_ A  /  x ]_ B
)  ->  { y  |  [. A  /  x ]. y  =  B }  =  { y  |  y  =  [_ A  /  x ]_ B }
)
1411, 13e1_ 28655 . . . . 5  |-  (. A  e.  V  ->.  { y  | 
[. A  /  x ]. y  =  B }  =  { y  |  y  =  [_ A  /  x ]_ B } ).
15 csbabg 3302 . . . . . . 7  |-  ( A  e.  V  ->  [_ A  /  x ]_ { y  |  y  =  B }  =  { y  |  [. A  /  x ]. y  =  B } )
1615eqcomd 2440 . . . . . 6  |-  ( A  e.  V  ->  { y  |  [. A  /  x ]. y  =  B }  =  [_ A  /  x ]_ { y  |  y  =  B } )
171, 16e1_ 28655 . . . . 5  |-  (. A  e.  V  ->.  { y  | 
[. A  /  x ]. y  =  B }  =  [_ A  /  x ]_ { y  |  y  =  B } ).
18 eqeq1 2441 . . . . . 6  |-  ( { y  |  [. A  /  x ]. y  =  B }  =  [_ A  /  x ]_ {
y  |  y  =  B }  ->  ( { y  |  [. A  /  x ]. y  =  B }  =  {
y  |  y  = 
[_ A  /  x ]_ B }  <->  [_ A  /  x ]_ { y  |  y  =  B }  =  { y  |  y  =  [_ A  /  x ]_ B } ) )
1918biimpcd 216 . . . . 5  |-  ( { y  |  [. A  /  x ]. y  =  B }  =  {
y  |  y  = 
[_ A  /  x ]_ B }  ->  ( { y  |  [. A  /  x ]. y  =  B }  =  [_ A  /  x ]_ {
y  |  y  =  B }  ->  [_ A  /  x ]_ { y  |  y  =  B }  =  { y  |  y  =  [_ A  /  x ]_ B } ) )
2014, 17, 19e11 28716 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { y  |  y  =  B }  =  { y  |  y  =  [_ A  /  x ]_ B } ).
21 df-sn 3812 . . . . . 6  |-  { B }  =  { y  |  y  =  B }
2221ax-gen 1555 . . . . 5  |-  A. x { B }  =  {
y  |  y  =  B }
23 csbeq2g 28563 . . . . 5  |-  ( A  e.  V  ->  ( A. x { B }  =  { y  |  y  =  B }  ->  [_ A  /  x ]_ { B }  =  [_ A  /  x ]_ {
y  |  y  =  B } ) )
241, 22, 23e10 28722 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { B }  =  [_ A  /  x ]_ { y  |  y  =  B } ).
25 eqeq2 2444 . . . . 5  |-  ( [_ A  /  x ]_ {
y  |  y  =  B }  =  {
y  |  y  = 
[_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ { B }  =  [_ A  /  x ]_ { y  |  y  =  B }  <->  [_ A  /  x ]_ { B }  =  { y  |  y  =  [_ A  /  x ]_ B } ) )
2625biimpd 199 . . . 4  |-  ( [_ A  /  x ]_ {
y  |  y  =  B }  =  {
y  |  y  = 
[_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ { B }  =  [_ A  /  x ]_ { y  |  y  =  B }  ->  [_ A  /  x ]_ { B }  =  {
y  |  y  = 
[_ A  /  x ]_ B } ) )
2720, 24, 26e11 28716 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { B }  =  { y  |  y  =  [_ A  /  x ]_ B } ).
28 df-sn 3812 . . 3  |-  { [_ A  /  x ]_ B }  =  { y  |  y  =  [_ A  /  x ]_ B }
29 eqeq2 2444 . . . 4  |-  ( {
[_ A  /  x ]_ B }  =  {
y  |  y  = 
[_ A  /  x ]_ B }  ->  ( [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }  <->  [_ A  /  x ]_ { B }  =  { y  |  y  =  [_ A  /  x ]_ B } ) )
3029biimprcd 217 . . 3  |-  ( [_ A  /  x ]_ { B }  =  {
y  |  y  = 
[_ A  /  x ]_ B }  ->  ( { [_ A  /  x ]_ B }  =  {
y  |  y  = 
[_ A  /  x ]_ B }  ->  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }
) )
3127, 28, 30e10 28722 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B } ).
3231in1 28589 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549    = wceq 1652    e. wcel 1725   {cab 2421   [.wsbc 3153   [_csb 3243   {csn 3806
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-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sbc 3154  df-csb 3244  df-sn 3812  df-vd1 28588
  Copyright terms: Public domain W3C validator