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

Theorem csbsngVD 28347
Description: Virtual deduction proof of csbsng 3811. 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 3811 is csbsngVD 28347 without virtual deductions and was automatically derived from csbsngVD 28347.
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 28007 . . . . . . . . 9  |-  (. A  e.  V  ->.  A  e.  V ).
2 sbceqg 3211 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [. A  /  x ]. y  =  B  <->  [_ A  /  x ]_ y  =  [_ A  /  x ]_ B ) )
31, 2e1_ 28070 . . . . . . . 8  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  =  B  <->  [_ A  /  x ]_ y  =  [_ A  /  x ]_ B ) ).
4 csbconstg 3209 . . . . . . . . . 10  |-  ( A  e.  V  ->  [_ A  /  x ]_ y  =  y )
51, 4e1_ 28070 . . . . . . . . 9  |-  (. A  e.  V  ->.  [_ A  /  x ]_ y  =  y ).
6 eqeq1 2394 . . . . . . . . 9  |-  ( [_ A  /  x ]_ y  =  y  ->  ( [_ A  /  x ]_ y  =  [_ A  /  x ]_ B  <->  y  =  [_ A  /  x ]_ B
) )
75, 6e1_ 28070 . . . . . . . 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 28131 . . . . . . 7  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  =  B  <->  y  =  [_ A  /  x ]_ B
) ).
1110gen11 28059 . . . . . 6  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. y  =  B  <->  y  =  [_ A  /  x ]_ B
) ).
12 abbi 2498 . . . . . . 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_ 28070 . . . . 5  |-  (. A  e.  V  ->.  { y  | 
[. A  /  x ]. y  =  B }  =  { y  |  y  =  [_ A  /  x ]_ B } ).
15 csbabg 3254 . . . . . . 7  |-  ( A  e.  V  ->  [_ A  /  x ]_ { y  |  y  =  B }  =  { y  |  [. A  /  x ]. y  =  B } )
1615eqcomd 2393 . . . . . 6  |-  ( A  e.  V  ->  { y  |  [. A  /  x ]. y  =  B }  =  [_ A  /  x ]_ { y  |  y  =  B } )
171, 16e1_ 28070 . . . . 5  |-  (. A  e.  V  ->.  { y  | 
[. A  /  x ]. y  =  B }  =  [_ A  /  x ]_ { y  |  y  =  B } ).
18 eqeq1 2394 . . . . . 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 28131 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { y  |  y  =  B }  =  { y  |  y  =  [_ A  /  x ]_ B } ).
21 df-sn 3764 . . . . . 6  |-  { B }  =  { y  |  y  =  B }
2221ax-gen 1552 . . . . 5  |-  A. x { B }  =  {
y  |  y  =  B }
23 csbeq2g 27980 . . . . 5  |-  ( A  e.  V  ->  ( A. x { B }  =  { y  |  y  =  B }  ->  [_ A  /  x ]_ { B }  =  [_ A  /  x ]_ {
y  |  y  =  B } ) )
241, 22, 23e10 28137 . . . 4  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { B }  =  [_ A  /  x ]_ { y  |  y  =  B } ).
25 eqeq2 2397 . . . . 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 28131 . . 3  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { B }  =  { y  |  y  =  [_ A  /  x ]_ B } ).
28 df-sn 3764 . . 3  |-  { [_ A  /  x ]_ B }  =  { y  |  y  =  [_ A  /  x ]_ B }
29 eqeq2 2397 . . . 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 28137 . 2  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B } ).
3231in1 28004 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546    = wceq 1649    e. wcel 1717   {cab 2374   [.wsbc 3105   [_csb 3195   {csn 3758
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-sbc 3106  df-csb 3196  df-sn 3764  df-vd1 28003
  Copyright terms: Public domain W3C validator