HomeHome Metamath Proof Explorer
Theorem List (p. 279 of 315)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21459)
  Hilbert Space Explorer  Hilbert Space Explorer
(21460-22982)
  Users' Mathboxes  Users' Mathboxes
(22983-31404)
 

Theorem List for Metamath Proof Explorer - 27801-27900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcsbeq2gVD 27801 Virtual deduction proof of csbeq2g 27451. 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. csbeq2g 27451 is csbeq2gVD 27801 without virtual deductions and was automatically derived from csbeq2gVD 27801.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  ( A. x B  =  C  ->  [. A  /  x ].  B  =  C ) ).
3:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. B  =  C  <->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) ).
4:2,3:  |-  (. A  e.  V  ->.  ( A. x B  =  C  ->  [_ A  /  x  ]_ B  =  [_ A  /  x ]_ C ) ).
qed:4:  |-  ( A  e.  V  ->  ( A. x B  =  C  ->  [_ A  /  x ]_  B  =  [_ A  /  x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  V  ->  (
 A. x  B  =  C  ->  [_ A  /  x ]_ B  =  [_ A  /  x ]_ C ) )
 
TheoremcsbsngVD 27802 Virtual deduction proof of csbsng 3666. 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 3666 is csbsngVD 27802 without virtual deductions and was automatically derived from csbsngVD 27802.
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.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ { B }  =  { [_ A  /  x ]_ B } )
 
TheoremcsbxpgVD 27803 Virtual deduction proof of csbxpg 4704. 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. csbxpg 4704 is csbxpgVD 27803 without virtual deductions and was automatically derived from csbxpgVD 27803.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. w  e.  B  <->  [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B ) ).
3:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ w  =  w ).
4:3:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ w  e.  [_ A  /  x ]_ B  <->  w  e.  [_ A  /  x ]_ B ) ).
5:2,4:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. w  e.  B  <->  w  e.  [_ A  /  x ]_ B ) ).
6:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  C  <->  [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C ) ).
7:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ y  =  y ).
8:7:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ y  e.  [_ A  /  x ]_ C  <->  y  e.  [_ A  /  x ]_ C ) ).
9:6,8:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) ).
10:5,9:  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ).
11:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C )  <->  ( [. A  /  x ]. w  e.  B  /\  [. A  /  x ]. y  e.  C ) ) ).
12:10,11:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( w  e.  B  /\  y  e.  C )  <->  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ).
13:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. z  =  <. w ,.  y >.  <->  z  =  <. w ,  y >. ) ).
14:12,13:  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. z  =  <. w  ,. y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
15:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  =  <. w  ,. y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( [. A  /  x ]. z  =  <. w ,  y >.  /\  [. A  /  x ]. ( w  e.  B  /\  y  e.  C ) ) ) ).
16:14,15:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  =  <. w  ,. y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
17:16:  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
18:17:  |-  (. A  e.  V  ->.  ( E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
19:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y [. A  /  x ]. ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) ) ).
20:18,19:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
21:20:  |-  (. A  e.  V  ->.  A. w ( [. A  /  x ]. E. y (  z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
22:21:  |-  (. A  e.  V  ->.  ( E. w [. A  /  x ]. E. y (  z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
23:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w E. y (  z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w [. A  /  x ]. E. y  ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) ) ).
24:22,23:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. w E. y (  z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
25:24:  |-  (. A  e.  V  ->.  A. z ( [. A  /  x ]. E. w E.  y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) )  <->  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) ) ).
26:25:  |-  (. A  e.  V  ->.  { z  |  [. A  /  x ]. E. w E.  y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  E. w E. y (  z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ).
27:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. w E.  y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  [. A  /  x ].  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) } ).
28:26,27:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. w E.  y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }  =  { z  |  E. w E. y (  z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }  ).
29::  |-  { <. w ,. y >.  |  ( w  e.  B  /\  y  e.  C ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }
30::  |-  ( B  X.  C )  =  { <. w ,. y >.  |  ( w  e.  B  /\  y  e.  C ) }
31:29,30:  |-  ( B  X.  C )  =  { z  |  E. w E. y ( z  =  <. w  ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }
32:31:  |-  A. x ( B  X.  C )  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) }
33:1,32:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C )  =  [_ A  /  x ]_ { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  B  /\  y  e.  C ) ) } ).
34:28,33:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C )  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) } ).
35::  |-  { <. w ,. y >.  |  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) }  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }
36::  |-  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C )  =  {  <. w ,  y >.  |  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) }
37:35,36:  |-  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C )  =  { z  |  E. w E. y ( z  =  <. w ,  y >.  /\  ( w  e.  [_ A  /  x ]_ B  /\  y  e.  [_ A  /  x ]_ C ) ) }
38:34,37:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  X.  C )  =  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C ) ).
qed:38:  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  X.  C )  =  (  [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  X.  C )  =  ( [_ A  /  x ]_ B  X.  [_ A  /  x ]_ C ) )
 
TheoremcsbresgVD 27804 Virtual deduction proof of csbresg 4946. 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. csbresg 4946 is csbresgVD 27804 without virtual deductions and was automatically derived from csbresgVD 27804.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ _V  =  _V ).
3:2:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
4:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  [_ A  /  x ]_ _V ) ).
5:3,4:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( C  X.  _V )  =  ( [_ A  /  x ]_ C  X.  _V ) ).
6:5:  |-  (. A  e.  V  ->.  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) ) ).
7:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  [_ A  /  x ]_ ( C  X.  _V ) ) ).
8:6,7:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) )  =  ( [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) ) ).
9::  |-  ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
10:9:  |-  A. x ( B  |`  C )  =  ( B  i^i  ( C  X.  _V ) )
11:1,10:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  [_ A  /  x ]_ ( B  i^i  ( C  X.  _V ) ) ).
12:8,11:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  (  [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) ) ).
13::  |-  ( [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C )  =  (  [_ A  /  x ]_ B  i^i  ( [_ A  /  x ]_ C  X.  _V ) )
14:12,13:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ ( B  |`  C )  =  (  [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) ).
qed:14:  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  |`  C )  =  (  [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ ( B  |`  C )  =  ( [_ A  /  x ]_ B  |`  [_ A  /  x ]_ C ) )
 
TheoremcsbrngVD 27805 Virtual deduction proof of csbrng 4911. 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 4911 is csbrngVD 27805 without virtual deductions and was automatically derived from csbrngVD 27805.
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.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ ran  B  =  ran  [_  A  /  x ]_ B )
 
Theoremcsbima12gALTVD 27806 Virtual deduction proof of csbima12gALT 5011. 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. csbima12gALT 5011 is csbima12gALTVD 27806 without virtual deductions and was automatically derived from csbima12gALTVD 27806.
1::  |-  (. A  e.  C  ->.  A  e.  C ).
2:1:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F  |`  B )  =  (  [_ A  /  x ]_ F  |`  [_ A  /  x ]_ B ) ).
3:2:  |-  (. A  e.  C  ->.  ran  [_ A  /  x ]_ ( F  |`  B )  =  ran  ( [_ A  /  x ]_ F  |`  [_ A  /  x ]_ B ) ).
4:1:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ran  ( F  |`  B )  =  ran  [_ A  /  x ]_ ( F  |`  B ) ).
5:3,4:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ran  ( F  |`  B )  =  ran  ( [_ A  /  x ]_ F  |`  [_ A  /  x ]_ B ) ).
6::  |-  ( F " B )  =  ran  ( F  |`  B )
7:6:  |-  A. x ( F " B )  =  ran  ( F  |`  B )
8:1,7:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " B )  =  [_  A  /  x ]_ ran  ( F  |`  B ) ).
9:5,8:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " B )  =  ran  ( [_ A  /  x ]_ F  |`  [_ A  /  x ]_ B ) ).
10::  |-  ( [_ A  /  x ]_ F " [_ A  /  x ]_ B )  =  ran  ( [_ A  /  x ]_ F  |`  [_ A  /  x ]_ B )
11:9,10:  |-  (. A  e.  C  ->.  [_ A  /  x ]_ ( F " B )  =  (  [_ A  /  x ]_ F " [_ A  /  x ]_ B ) ).
qed:11:  |-  ( 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.)
 |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F " B )  =  ( [_ A  /  x ]_ F " [_ A  /  x ]_ B ) )
 
TheoremcsbunigVD 27807 Virtual deduction proof of csbunig 3809. 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. csbunig 3809 is csbunigVD 27807 without virtual deductions and was automatically derived from csbunigVD 27807.
1::  |-  (. A  e.  V  ->.  A  e.  V ).
2:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
3:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. y  e.  B  <->  y  e.  [_ A  /  x ]_ B ) ).
4:2,3:  |-  (. A  e.  V  ->.  ( ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
5:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( [. A  /  x ]. z  e.  y  /\  [. A  /  x ]. y  e.  B ) ) ).
6:4,5:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
7:6:  |-  (. A  e.  V  ->.  A. y ( [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
8:7:  |-  (. A  e.  V  ->.  ( E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B )  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
9:1:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y [. A  /  x ]. ( z  e.  y  /\  y  e.  B ) ) ).
10:8,9:  |-  (. A  e.  V  ->.  ( [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B )  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
11:10:  |-  (. A  e.  V  ->.  A. z ( [. A  /  x ]. E. y (  z  e.  y  /\  y  e.  B )  <->  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) ) ).
12:11:  |-  (. A  e.  V  ->.  { z  |  [. A  /  x ]. E. y (  z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) } ).
13:1:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  [. A  /  x ]. E. y ( z  e.  y  /\  y  e.  B ) }  ).
14:12,13:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) }  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) } ).
15::  |-  U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) }
16:15:  |-  A. x U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) }
17:1,16:  |-  (. A  e.  V  ->.  [. A  /  x ]. U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  B ) } ).
18:1,17:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  [_ A  /  x ]_ { z  |  E. y ( z  e.  y  /\  y  e.  B ) } ).
19:14,18:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) } ).
20::  |-  U. [_ A  /  x ]_ B  =  { z  |  E. y ( z  e.  y  /\  y  e.  [_ A  /  x ]_ B ) }
21:19,20:  |-  (. A  e.  V  ->.  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B ).
qed:21:  |-  ( A  e.  V  ->  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B )
(Contributed by Alan Sare, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ U. B  =  U. [_ A  /  x ]_ B )
 
Theoremcsbfv12gALTVD 27808 Virtual deduction proof of csbfv12gALT 5469. 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. csbfv12gALT 5469 is csbfv12gALTVD 27808 without virtual deductions and was automatically derived from csbfv12gALTVD 27808.
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.)
 |-  ( A  e.  C  ->  [_ A  /  x ]_ ( F `  B )  =  ( [_ A  /  x ]_ F `  [_ A  /  x ]_ B ) )
 
Theoremcon5VD 27809 Virtual deduction proof of con5 27421. 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. con5 27421 is con5VD 27809 without virtual deductions and was automatically derived from con5VD 27809.
1::  |-  (. ( ph  <->  -.  ps )  ->.  ( ph  <->  -.  ps ) ).
2:1:  |-  (. ( ph  <->  -.  ps )  ->.  ( -.  ps  ->  ph ) ).
3:2:  |-  (. ( ph  <->  -.  ps )  ->.  ( -.  ph  ->  -.  -.  ps  ) ).
4::  |-  ( ps  <->  -.  -.  ps )
5:3,4:  |-  (. ( ph  <->  -.  ps )  ->.  ( -.  ph  ->  ps ) ).
qed:5:  |-  ( ( ph  <->  -.  ps )  ->  ( -.  ph  ->  ps ) )
(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  <->  -.  ps )  ->  ( -.  ph  ->  ps )
 )
 
TheoremrelopabVD 27810 Virtual deduction proof of relopab 4800. 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. relopab 4800 is relopabVD 27810 without virtual deductions and was automatically derived from relopabVD 27810.
1::  |-  (. y  =  v  ->.  y  =  v ).
2:1:  |-  (. y  =  v  ->.  <. x ,. y >.  =  <. x ,. v  >. ).
3::  |-  (. y  =  v ,. x  =  u  ->.  x  =  u ).
4:3:  |-  (. y  =  v ,. x  =  u  ->.  <. x ,. v >.  =  <.  u ,  v >. ).
5:2,4:  |-  (. y  =  v ,. x  =  u  ->.  <. x ,. y >.  =  <.  u ,  v >. ).
6:5:  |-  (. y  =  v ,. x  =  u  ->.  ( z  =  <. x ,. y  >.  ->  z  =  <. u ,  v >. ) ).
7:6:  |-  (. y  =  v  ->.  ( x  =  u  ->  ( z  =  <. x ,.  y >.  ->  z  =  <. u ,  v >. ) ) ).
8:7:  |-  ( y  =  v  ->  ( x  =  u  ->  ( z  =  <. x ,. y  >.  ->  z  =  <. u ,  v >. ) ) )
9:8:  |-  ( E. v y  =  v  ->  E. v ( x  =  u  ->  ( z  =  <. x ,  y >.  ->  z  =  <. u ,  v >. ) ) )
90::  |-  ( v  =  y  <->  y  =  v )
91:90:  |-  ( E. v v  =  y  <->  E. v y  =  v )
92::  |-  E. v v  =  y
10:91,92:  |-  E. v y  =  v
11:9,10:  |-  E. v ( x  =  u  ->  ( z  =  <. x ,. y >.  ->  z  =  <. u ,  v >. ) )
12:11:  |-  ( x  =  u  ->  E. v ( z  =  <. x ,. y >.  ->  z  =  <. u ,  v >. ) )
13::  |-  ( E. v ( z  =  <. x ,. y >.  ->  z  =  <. u  ,  v >. )  ->  ( z  =  <. x ,  y >.  ->  E. v z  =  <. u ,  v >. ) )
14:12,13:  |-  ( x  =  u  ->  ( z  =  <. x ,. y >.  ->  E. v  z  =  <. u ,  v >. ) )
15:14:  |-  ( E. u x  =  u  ->  E. u ( z  =  <. x ,. y  >.  ->  E. v z  =  <. u ,  v >. ) )
150::  |-  ( u  =  x  <->  x  =  u )
151:150:  |-  ( E. u u  =  x  <->  E. u x  =  u )
152::  |-  E. u u  =  x
16:151,152:  |-  E. u x  =  u
17:15,16:  |-  E. u ( z  =  <. x ,. y >.  ->  E. v z  =  <.  u ,  v >. )
18:17:  |-  ( z  =  <. x ,. y >.  ->  E. u E. v z  =  <.  u ,  v >. )
19:18:  |-  ( E. y z  =  <. x ,. y >.  ->  E. y E. u  E. v z  =  <. u ,  v >. )
20::  |-  ( E. y E. u E. v z  =  <. u ,. v >.  ->  E. u E. v z  =  <. u ,  v >. )
21:19,20:  |-  ( E. y z  =  <. x ,. y >.  ->  E. u E. v z  =  <. u ,  v >. )
22:21:  |-  ( E. x E. y z  =  <. x ,. y >.  ->  E. x  E. u E. v z  =  <. u ,  v >. )
23::  |-  ( E. x E. u E. v z  =  <. u ,. v >.  ->  E. u E. v z  =  <. u ,  v >. )
24:22,23:  |-  ( E. x E. y z  =  <. x ,. y >.  ->  E. u  E. v z  =  <. u ,  v >. )
25:24:  |-  { z  |  E. x E. y z  =  <. x ,. y >. }  C_  { z  |  E. u E. v z  =  <. u ,  v >. }
26::  |-  x  e.  _V
27::  |-  y  e.  _V
28:26,27:  |-  ( x  e.  _V  /\  y  e.  _V )
29:28:  |-  ( z  =  <. x ,. y >.  <->  ( z  =  <. x ,. y  >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) )
30:29:  |-  ( E. y z  =  <. x ,. y >.  <->  E. y ( z  =  <. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) )
31:30:  |-  ( E. x E. y z  =  <. x ,. y >.  <->  E. x  E. y ( z  =  <. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) )
32:31:  |-  { z  |  E. x E. y z  =  <. x ,. y >. }  =  {  z  |  E. x E. y ( z  =  <. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) }
320:25,32:  |-  { z  |  E. x E. y ( z  =  <. x ,. y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) }  C_  { z  |  E. u E. v z  =  <. u ,  v >. }
33::  |-  u  e.  _V
34::  |-  v  e.  _V
35:33,34:  |-  ( u  e.  _V  /\  v  e.  _V )
36:35:  |-  ( z  =  <. u ,. v >.  <->  ( z  =  <. u ,. v  >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) )
37:36:  |-  ( E. v z  =  <. u ,. v >.  <->  E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) )
38:37:  |-  ( E. u E. v z  =  <. u ,. v >.  <->  E. u  E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) )
39:38:  |-  { z  |  E. u E. v z  =  <. u ,. v >. }  =  {  z  |  E. u E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) }
40:320,39:  |-  { z  |  E. x E. y ( z  =  <. x ,. y >.  /\  ( x  e.  _V  /\  y  e.  _V ) ) }  C_  { z  |  E. u E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) ) }
41::  |-  { <. x ,. y >.  |  ( x  e.  _V  /\  y  e.  _V  ) }  =  { z  |  E. x E. y ( z  =  <. x ,  y >.  /\  ( x  e.  _V  /\  y  e.  _V ) )  }
42::  |-  { <. u ,. v >.  |  ( u  e.  _V  /\  v  e.  _V  ) }  =  { z  |  E. u E. v ( z  =  <. u ,  v >.  /\  ( u  e.  _V  /\  v  e.  _V ) )  }
43:40,41,42:  |-  { <. x ,. y >.  |  ( x  e.  _V  /\  y  e.  _V  ) }  C_  { <. u ,  v >.  |  ( u  e.  _V  /\  v  e.  _V ) }
44::  |-  { <. u ,. v >.  |  ( u  e.  _V  /\  v  e.  _V  ) }  =  ( _V  X.  _V )
45:43,44:  |-  { <. x ,. y >.  |  ( x  e.  _V  /\  y  e.  _V  ) }  C_  ( _V  X.  _V )
46:28:  |-  ( ph  ->  ( x  e.  _V  /\  y  e.  _V ) )
47:46:  |-  { <. x ,. y >.  |  ph }  C_  { <. x ,. y >.  |  ( x  e.  _V  /\  y  e.  _V ) }
48:45,47:  |-  { <. x ,. y >.  |  ph }  C_  ( _V  X.  _V )
qed:48:  |-  Rel  { <. x ,. y >.  |  ph }
(Contributed by Alan Sare, 9-Jul-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  Rel  {
 <. x ,  y >.  | 
 ph }
 
Theorem19.41rgVD 27811 Virtual deduction proof of 19.41rg 27452. 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. 19.41rg 27452 is 19.41rgVD 27811 without virtual deductions and was automatically derived from 19.41rgVD 27811. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  ( ps  ->  ( ph  ->  ( ph  /\  ps ) ) )
2:1:  |-  ( ( ps  ->  A. x ps )  ->  ( ps  ->  ( ph  ->  (  ph  /\  ps ) ) ) )
3:2:  |-  A. x ( ( ps  ->  A. x ps )  ->  ( ps  ->  ( ph  ->  ( ph  /\  ps ) ) ) )
4:3:  |-  ( A. x ( ps  ->  A. x ps )  ->  ( A. x ps  ->  A. x ( ph  ->  ( ph  /\  ps ) ) ) )
5::  |-  (. A. x ( ps  ->  A. x ps )  ->.  A. x ( ps  ->  A. x ps ) ).
6:4,5:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  A. x ( ph  ->  ( ph  /\  ps ) ) ) ).
7::  |-  (. A. x ( ps  ->  A. x ps ) ,. A. x ps  ->.  A. x ps ).
8:6,7:  |-  (. A. x ( ps  ->  A. x ps ) ,. A. x ps  ->.  A. x ( ph  ->  ( ph  /\  ps ) ) ).
9:8:  |-  (. A. x ( ps  ->  A. x ps ) ,. A. x ps  ->.  ( E. x ph  ->  E. x ( ph  /\  ps ) ) ).
10:9:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( A. x ps  ->  ( E. x ph  ->  E. x ( ph  /\  ps ) ) ) ).
11:5:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  A.  x ps ) ).
12:10,11:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ps  ->  (  E. x ph  ->  E. x ( ph  /\  ps ) ) ) ).
13:12:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( E. x ph  ->  ( ps  ->  E. x ( ph  /\  ps ) ) ) ).
14:13:  |-  (. A. x ( ps  ->  A. x ps )  ->.  ( ( E. x  ph  /\  ps )  ->  E. x ( ph  /\  ps ) ) ).
qed:14:  |-  ( A. x ( ps  ->  A. x ps )  ->  ( ( E. x ph  /\  ps )  ->  E. x ( ph  /\  ps ) ) )
 |-  ( A. x ( ps  ->  A. x ps )  ->  ( ( E. x ph 
 /\  ps )  ->  E. x ( ph  /\  ps )
 ) )
 
Theorem2pm13.193VD 27812 Virtual deduction proof of 2pm13.193 27454. 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. 2pm13.193 27454 is 2pm13.193VD 27812 without virtual deductions and was automatically derived from 2pm13.193VD 27812. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) ).
2:1:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  ( x  =  u  /\  y  =  v ) ).
3:2:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  x  =  u ).
4:1:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  [ u  /  x ] [ v  /  y ] ph ).
5:3,4:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  ( [ u  /  x ] [ v  /  y ] ph  /\  x  =  u ) ).
6:5:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  ( [ v  /  y ] ph  /\  x  =  u ) ).
7:6:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  [ v  /  y ] ph ).
8:2:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  y  =  v ).
9:7,8:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  ( [ v  /  y ] ph  /\  y  =  v ) ).
10:9:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  ( ph  /\  y  =  v ) ).
11:10:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  ph ).
12:2,11:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
13:12:  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  ->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
14::  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( (  x  =  u  /\  y  =  v )  /\  ph ) ).
15:14:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( x  =  u  /\  y  =  v ) ).
16:15:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  y  =  v ).
17:14:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  ph  ).
18:16,17:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  (  ph  /\  y  =  v ) ).
19:18:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [  v  /  y ] ph  /\  y  =  v ) ).
20:15:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  x  =  u ).
21:19:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  [ v  /  y ] ph ).
22:20,21:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [  v  /  y ] ph  /\  x  =  u ) ).
23:22:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( [  u  /  x ] [ v  /  y ] ph  /\  x  =  u ) ).
24:23:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  [ u  /  x ] [ v  /  y ] ph ).
25:15,24:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ph )  ->.  ( (  x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) ).
26:25:  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ph )  ->  ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
qed:13,26:  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
 |-  (
 ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [
 v  /  y ] ph )  <->  ( ( x  =  u  /\  y  =  v )  /\  ph )
 )
 
TheoremhbimpgVD 27813 Virtual deduction proof of hbimpg 27456. 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. hbimpg 27456 is hbimpgVD 27813 without virtual deductions and was automatically derived from hbimpgVD 27813. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ).
2:1:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ph  ->  A. x ph ) ).
3::  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,  -.  ph  ->.  -.  ph ).
4:2:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( -.  ph  ->  A. x -.  ph ) ).
5:4:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x -.  ph ) ).
6:3,5:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,  -.  ph  ->.  A. x -.  ph ).
7::  |-  ( -.  ph  ->  ( ph  ->  ps ) )
8:7:  |-  ( A. x -.  ph  ->  A. x ( ph  ->  ps ) )
9:6,8:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) ,  -.  ph  ->.  A. x ( ph  ->  ps ) ).
10:9:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( -.  ph  ->  A. x ( ph  ->  ps ) ) ).
11::  |-  ( ps  ->  ( ph  ->  ps ) )
12:11:  |-  ( A. x ps  ->  A. x ( ph  ->  ps ) )
13:1:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ps  ->  A. x ps ) ).
14:13:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x ps ) ).
15:14,12:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ps  ->  A. x ( ph  ->  ps ) ) ).
16:10,15:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( -.  ph  \/  ps )  ->  A. x ( ph  ->  ps ) ) ).
17::  |-  ( ( ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
18:16,17:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  ( ( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) ).
19::  |-  ( A. x ( ph  ->  A. x ph )  ->  A. x A. x (  ph  ->  A. x ph ) )
20::  |-  ( A. x ( ps  ->  A. x ps )  ->  A. x A. x (  ps  ->  A. x ps ) )
21:19,20:  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->  A. x ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) ) )
22:21,18:  |-  (. ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->.  A. x ( ( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) ).
qed:22:  |-  ( ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps  ->  A. x ps ) )  ->  A. x ( ( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) )
 |-  (
 ( A. x ( ph  ->  A. x ph )  /\  A. x ( ps 
 ->  A. x ps )
 )  ->  A. x ( ( ph  ->  ps )  ->  A. x ( ph  ->  ps ) ) )
 
TheoremhbalgVD 27814 Virtual deduction proof of hbalg 27457. 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. hbalg 27457 is hbalgVD 27814 without virtual deductions and was automatically derived from hbalgVD 27814. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y ( ph  ->  A. x ph ) ).
2:1:  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. y A. x ph ) ).
3::  |-  ( A. y A. x ph  ->  A. x A. y ph )
4:2,3:  |-  (. A. y ( ph  ->  A. x ph )  ->.  ( A. y ph  ->  A. x A. y ph ) ).
5::  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y A. y (  ph  ->  A. x ph ) )
6:5,4:  |-  (. A. y ( ph  ->  A. x ph )  ->.  A. y ( A.  y ph  ->  A. x A. y ph ) ).
qed:6:  |-  ( A. y ( ph  ->  A. x ph )  ->  A. y ( A. y  ph  ->  A. x A. y ph ) )
 |-  ( A. y ( ph  ->  A. x ph )  ->  A. y ( A. y ph  ->  A. x A. y ph ) )
 
TheoremhbexgVD 27815 Virtual deduction proof of hbexg 27458. 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. hbexg 27458 is hbexgVD 27815 without virtual deductions and was automatically derived from hbexgVD 27815. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  A. y ( ph  ->  A. x ph ) ).
2:1:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  A. x ( ph  ->  A. x ph ) ).
3:2:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  ( ph  ->  A. x ph ) ).
4:3:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  ( -.  ph  ->  A. x -.  ph ) ).
5::  |-  ( A. x A. y ( ph  ->  A. x ph )  <->  A. y  A. x ( ph  ->  A. x ph ) )
6::  |-  ( A. y A. x ( ph  ->  A. x ph )  ->  A. y  A. y A. x ( ph  ->  A. x ph ) )
7:5:  |-  ( A. y A. x A. y ( ph  ->  A. x ph )  <->  A. y A. y A. x ( ph  ->  A. x ph ) )
8:5,6,7:  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. y  A. x A. y ( ph  ->  A. x ph ) )
9:8,4:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  A. x ( -.  ph  ->  A. x -.  ph ) ).
10:9:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  A. y ( -.  ph  ->  A. x -.  ph ) ).
11:10:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  ( -.  ph  ->  A. x -.  ph ) ).
12:11:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  ( A. y -.  ph  ->  A. x A. y -.  ph ) ).
13:12:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( A.  y -.  ph  ->  A. x A. y -.  ph ) ).
14::  |-  ( A. x A. y ( ph  ->  A. x ph )  ->  A. x  A. x A. y ( ph  ->  A. x ph ) )
15:13,14:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  ( A. y -.  ph  ->  A. x A. y -.  ph ) ).
16:15:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  ( -.  A. y -.  ph  ->  A. x -.  A. y -.  ph ) ).
17:16:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( -.  A. y -.  ph  ->  A. x -.  A. y -.  ph ) ).
18::  |-  ( E. y ph  <->  -.  A. y -.  ph )
19:17,18:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E.  y ph  ->  A. x -.  A. y -.  ph ) ).
20:18:  |-  ( A. x E. y ph  <->  A. x -.  A. y -.  ph )
21:19,20:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  ( E.  y ph  ->  A. x E. y ph ) ).
22:8,21:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. y  ( E. y ph  ->  A. x E. y ph ) ).
23:14,22:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  A. y ( E. y ph  ->  A. x E. y ph ) ).
qed:23:  |-  (. A. x A. y ( ph  ->  A. x ph )  ->.  A. x  A. y ( E. y ph  ->  A. x E. y ph ) ).
 |-  ( A. x A. y (
 ph  ->  A. x ph )  ->  A. x A. y
 ( E. y ph  ->  A. x E. y ph ) )
 
Theorema9e2eqVD 27816* The following User's Proof is a Virtual Deduction proof (see: wvd1 27473) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. a9e2eq 27459 is a9e2eqVD 27816 without virtual deductions and was automatically derived from a9e2eqVD 27816. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. A. x x  =  y  ->.  A. x x  =  y ).
2::  |-  (. A. x x  =  y ,. x  =  u  ->.  x  =  u ).
3:1:  |-  (. A. x x  =  y  ->.  x  =  y ).
4:2,3:  |-  (. A. x x  =  y ,. x  =  u  ->.  y  =  u ).
5:2,4:  |-  (. A. x x  =  y ,. x  =  u  ->.  ( x  =  u  /\  y  =  u ) ).
6:5:  |-  (. A. x x  =  y  ->.  ( x  =  u  ->  ( x  =  u  /\  y  =  u ) ) ).
7:6:  |-  ( A. x x  =  y  ->  ( x  =  u  ->  ( x  =  u  /\  y  =  u ) ) )
8:7:  |-  ( A. x A. x x  =  y  ->  A. x ( x  =  u  ->  (  x  =  u  /\  y  =  u ) ) )
9::  |-  ( A. x x  =  y  <->  A. x A. x x  =  y )
10:8,9:  |-  ( A. x x  =  y  ->  A. x ( x  =  u  ->  ( x  =  u  /\  y  =  u ) ) )
11:1,10:  |-  (. A. x x  =  y  ->.  A. x ( x  =  u  ->  ( x  =  u  /\  y  =  u ) ) ).
12:11:  |-  (. A. x x  =  y  ->.  ( E. x x  =  u  ->  E. x  ( x  =  u  /\  y  =  u ) ) ).
13::  |-  E. x x  =  u
14:13,12:  |-  (. A. x x  =  y  ->.  E. x ( x  =  u  /\  y  =  u  ) ).
140:14:  |-  ( A. x x  =  y  ->  E. x ( x  =  u  /\  y  =  u )  )
141:140:  |-  ( A. x x  =  y  ->  A. x E. x ( x  =  u  /\  y  =  u ) )
15:1,141:  |-  (. A. x x  =  y  ->.  A. x E. x ( x  =  u  /\  y  =  u ) ).
16:1,15:  |-  (. A. x x  =  y  ->.  A. y E. x ( x  =  u  /\  y  =  u ) ).
17:16:  |-  (. A. x x  =  y  ->.  E. y E. x ( x  =  u  /\  y  =  u ) ).
18:17:  |-  (. A. x x  =  y  ->.  E. x E. y ( x  =  u  /\  y  =  u ) ).
19::  |-  (. u  =  v  ->.  u  =  v ).
20::  |-  (. u  =  v ,. ( x  =  u  /\  y  =  u )  ->.  ( x  =  u  /\  y  =  u ) ).
21:20:  |-  (. u  =  v ,. ( x  =  u  /\  y  =  u )  ->.  y  =  u  ).
22:19,21:  |-  (. u  =  v ,. ( x  =  u  /\  y  =  u )  ->.  y  =  v  ).
23:20:  |-  (. u  =  v ,. ( x  =  u  /\  y  =  u )  ->.  x  =  u  ).
24:22,23:  |-  (. u  =  v ,. ( x  =  u  /\  y  =  u )  ->.  ( x  =  u  /\  y  =  v ) ).
25:24:  |-  (. u  =  v  ->.  ( ( x  =  u  /\  y  =  u )  ->  (  x  =  u  /\  y  =  v ) ) ).
26:25:  |-  (. u  =  v  ->.  A. y ( ( x  =  u  /\  y  =  u )  ->  ( x  =  u  /\  y  =  v ) ) ).
27:26:  |-  (. u  =  v  ->.  ( E. y ( x  =  u  /\  y  =  u )  ->  E. y ( x  =  u  /\  y  =  v ) ) ).
28:27:  |-  (. u  =  v  ->.  A. x ( E. y ( x  =  u  /\  y  =  u )  ->  E. y ( x  =  u  /\  y  =  v ) ) ).
29:28:  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  u )  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) ).
30:29:  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  u  )  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )
31:18,30:  |-  (. A. x x  =  y  ->.  ( u  =  v  ->  E. x E. y  ( x  =  u  /\  y  =  v ) ) ).
qed:31:  |-  ( A. x x  =  y  ->  ( u  =  v  ->  E. x E. y (  x  =  u  /\  y  =  v ) ) )
 |-  ( A. x  x  =  y  ->  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v ) ) )
 
Theorema9e2ndVD 27817* The following User's Proof is a Virtual Deduction proof (see: wvd1 27473) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. a9e2eq 27459 is a9e2ndVD 27817 without virtual deductions and was automatically derived from a9e2ndVD 27817. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  E. y y  =  v
2::  |-  u  e.  _V
3:1,2:  |-  ( u  e.  _V  /\  E. y y  =  v )
4:3:  |-  E. y ( u  e.  _V  /\  y  =  v )
5::  |-  ( u  e.  _V  <->  E. x x  =  u )
6:5:  |-  ( ( u  e.  _V  /\  y  =  v )  <->  ( E. x x  =  u  /\  y  =  v ) )
7:6:  |-  ( E. y ( u  e.  _V  /\  y  =  v )  <->  E. y  ( E. x x  =  u  /\  y  =  v ) )
8:4,7:  |-  E. y ( E. x x  =  u  /\  y  =  v )
9::  |-  ( z  =  v  ->  A. x z  =  v )
10::  |-  ( y  =  v  ->  A. z y  =  v )
11::  |-  (. z  =  y  ->.  z  =  y ).
12:11:  |-  (. z  =  y  ->.  ( z  =  v  <->  y  =  v ) ).
120:11:  |-  ( z  =  y  ->  ( z  =  v  <->  y  =  v ) )
13:9,10,120:  |-  ( -.  A. x x  =  y  ->  ( y  =  v  ->  A. x y  =  v ) )
14::  |-  (. -.  A. x x  =  y  ->.  -.  A. x x  =  y ).
15:14,13:  |-  (. -.  A. x x  =  y  ->.  ( y  =  v  ->  A. x  y  =  v ) ).
16:15:  |-  ( -.  A. x x  =  y  ->  ( y  =  v  ->  A. x y  =  v ) )
17:16:  |-  ( A. x -.  A. x x  =  y  ->  A. x ( y  =  v  ->  A. x y  =  v ) )
18::  |-  ( -.  A. x x  =  y  ->  A. x -.  A. x x  =  y  )
19:17,18:  |-  ( -.  A. x x  =  y  ->  A. x ( y  =  v  ->  A.  x y  =  v ) )
20:14,19:  |-  (. -.  A. x x  =  y  ->.  A. x ( y  =  v  ->  A. x y  =  v ) ).
21:20:  |-  (. -.  A. x x  =  y  ->.  ( ( E. x x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) ).
22:21:  |-  ( -.  A. x x  =  y  ->  ( ( E. x x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) )
23:22:  |-  ( A. y -.  A. x x  =  y  ->  A. y ( ( E. x  x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) )
24::  |-  ( -.  A. x x  =  y  ->  A. y -.  A. x x  =  y  )
25:23,24:  |-  ( -.  A. x x  =  y  ->  A. y ( ( E. x x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) )
26:14,25:  |-  (. -.  A. x x  =  y  ->.  A. y ( ( E. x x  =  u  /\  y  =  v )  ->  E. x ( x  =  u  /\  y  =  v ) ) ).
27:26:  |-  (. -.  A. x x  =  y  ->.  ( E. y ( E. x x  =  u  /\  y  =  v )  ->  E. y E. x ( x  =  u  /\  y  =  v ) ) ).
28:8,27:  |-  (. -.  A. x x  =  y  ->.  E. y E. x ( x  =  u  /\  y  =  v ) ).
29:28:  |-  (. -.  A. x x  =  y  ->.  E. x E. y ( x  =  u  /\  y  =  v ) ).
qed:29:  |-  ( -.  A. x x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
 |-  ( -.  A. x  x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
 
Theorema9e2ndeqVD 27818* The following User's Proof is a Virtual Deduction proof (see: wvd1 27473) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. a9e2eq 27459 is a9e2ndeqVD 27818 without virtual deductions and was automatically derived from a9e2ndeqVD 27818. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  (. u  =/=  v  ->.  u  =/=  v ).
2::  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  (  x  =  u  /\  y  =  v ) ).
3:2:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =  u ).
4:1,3:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  v ).
5:2:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  y  =  v ).
6:4,5:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  x  =/=  y ).
7::  |-  ( A. x x  =  y  ->  x  =  y )
8:7:  |-  ( -.  x  =  y  ->  -.  A. x x  =  y )
9::  |-  ( -.  x  =  y  <->  x  =/=  y )
10:8,9:  |-  ( x  =/=  y  ->  -.  A. x x  =  y )
11:6,10:  |-  (. u  =/=  v ,. ( x  =  u  /\  y  =  v )  ->.  -.  A. x x  =  y ).
12:11:  |-  (. u  =/=  v  ->.  ( ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
13:12:  |-  (. u  =/=  v  ->.  A. x ( ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
14:13:  |-  (. u  =/=  v  ->.  ( E. x ( x  =  u  /\  y  =  v )  ->  E. x -.  A. x x  =  y ) ).
15::  |-  ( -.  A. x x  =  y  ->  A. x -.  A. x x  =  y  )
19:15:  |-  ( E. x -.  A. x x  =  y  <->  -.  A. x x  =  y )
20:14,19:  |-  (. u  =/=  v  ->.  ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
21:20:  |-  (. u  =/=  v  ->.  A. y ( E. x ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
22:21:  |-  (. u  =/=  v  ->.  ( E. y E. x ( x  =  u  /\  y  =  v )  ->  E. y -.  A. x x  =  y ) ).
23::  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  <->  E.  y E. x ( x  =  u  /\  y  =  v ) )
24:22,23:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  E. y -.  A. x x  =  y ) ).
25::  |-  ( -.  A. x x  =  y  ->  A. y -.  A. x x  =  y  )
26:25:  |-  ( E. y -.  A. x x  =  y  ->  E. y A. y -.  A. x x  =  y )
260::  |-  ( A. y -.  A. x x  =  y  ->  A. y A. y -.  A. x x  =  y )
27:260:  |-  ( E. y A. y -.  A. x x  =  y  <->  A. y -.  A. x x  =  y )
270:26,27:  |-  ( E. y -.  A. x x  =  y  ->  A. y -.  A. x  x  =  y )
28::  |-  ( A. y -.  A. x x  =  y  ->  -.  A. x x  =  y  )
29:270,28:  |-  ( E. y -.  A. x x  =  y  ->  -.  A. x x  =  y  )
30:24,29:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  -.  A. x x  =  y ) ).
31:30:  |-  (. u  =/=  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) ).
32:31:  |-  ( u  =/=  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) )
33::  |-  (. u  =  v  ->.  u  =  v ).
34:33:  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  u  =  v ) ).
35:34:  |-  (. u  =  v  ->.  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) ).
36:35:  |-  ( u  =  v  ->  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( -.  A. x x  =  y  \/  u  =  v ) ) )
37::  |-  ( u  =  v  \/  u  =/=  v )
38:32,36,37:  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  (  -.  A. x x  =  y  \/  u  =  v ) )
39::  |-  ( A. x x  =  y  ->  ( u  =  v  ->  E. x E. y  ( x  =  u  /\  y  =  v ) ) )
40::  |-  ( -.  A. x x  =  y  ->  E. x E. y ( x  =  u  /\  y  =  v ) )
41:40:  |-  ( -.  A. x x  =  y  ->  ( u  =  v  ->  E. x E.  y ( x  =  u  /\  y  =  v ) ) )
42::  |-  ( A. x x  =  y  \/  -.  A. x x  =  y )
43:39,41,42:  |-  ( u  =  v  ->  E. x E. y ( x  =  u  /\  y  =  v  ) )
44:40,43:  |-  ( ( -.  A. x x  =  y  \/  u  =  v )  ->  E. x  E. y ( x  =  u  /\  y  =  v ) )
qed:38,44:  |-  ( ( -.  A. x x  =  y  \/  u  =  v )  <->  E. x  E. y ( x  =  u  /\  y  =  v ) )
 |-  (
 ( -.  A. x  x  =  y  \/  u  =  v )  <->  E. x E. y ( x  =  u  /\  y  =  v )
 )
 
Theorem2sb5ndVD 27819* The following User's Proof is a Virtual Deduction proof (see: wvd1 27473) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 27462 is 2sb5ndVD 27819 without virtual deductions and was automatically derived from 2sb5ndVD 27819. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1::  |-  ( ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [  v  /  y ] ph )  <->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
2:1:  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) )
3::  |-  ( [ v  /  y ] ph  ->  A. y [ v  /  y ] ph )
4:3:  |-  [ u  /  x ] ( [ v  /  y ] ph  ->  A. y [ v  /  y ] ph )
5:4:  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  [ u  /  x ]  A. y [ v  /  y ] ph )
6::  |-  (. -.  A. x x  =  y  ->.  -.  A. x x  =  y ).
7::  |-  ( A. y y  =  x  ->  A. x x  =  y )
8:7:  |-  ( -.  A. x x  =  y  ->  -.  A. y y  =  x )
9:6,8:  |-  (. -.  A. x x  =  y  ->.  -.  A. y y  =  x ).
10:9:  |-  ( [ u  /  x ] A. y [ v  /  y ] ph  <->  A.  y [ u  /  x ] [ v  /  y ] ph )
11:5,10:  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph )
12:11:  |-  ( -.  A. x x  =  y  ->  ( [ u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
13::  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. x [ u  /  x ] [ v  /  y ] ph )
14::  |-  (. A. x x  =  y  ->.  A. x x  =  y ).
15:14:  |-  (. A. x x  =  y  ->.  ( A. x [ u  /  x ] [  v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) ).
16:13,15:  |-  (. A. x x  =  y  ->.  ( [ u  /  x ] [ v  /  y  ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) ).
17:16:  |-  ( A. x x  =  y  ->  ( [ u  /  x ] [ v  /  y ]  ph  ->  A. y [ u  /  x ] [ v  /  y ] ph ) )
19:12,17:  |-  ( [ u  /  x ] [ v  /  y ] ph  ->  A. y [ u  /  x ] [ v  /  y ] ph )
20:19:  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  ( E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
21:2,20:  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  <->  ( E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
22:21:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  <->  E. x ( E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
23:13:  |-  ( E. x ( E. y ( x  =  u  /\  y  =  v )  /\  [  u  /  x ] [ v  /  y ] ph )  <->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
24:22,23:  |-  ( ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [  u  /  x ] [ v  /  y ] ph )  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) )
240:24:  |-  ( ( E. x E. y ( x  =  u  /\  y  =  v )  /\  (  E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )  <->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
241::  |-  ( ( E. x E. y ( x  =  u  /\  y  =  v )  /\  (  E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )  <->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph ) )
242:241,240:  |-  ( ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [  u  /  x ] [ v  /  y ] ph )  <->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
243::  |-  ( ( E. x E. y ( x  =  u  /\  y  =  v )  ->  (  [ u  /  x ] [ v  /  y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )  <->  ( ( E. x E. y ( x  =  u  /\  y  =  v )  /\  [ u  /  x ] [ v  /  y ] ph )  <->  ( E. x E. y ( x  =  u  /\  y  =  v )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) ) )
25:242,243:  |-  ( E. x E. y ( x  =  u  /\  y  =  v )  ->  ( [  u  /  x ] [ v  /  y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
26::  |-  ( ( -.  A. x x  =  y  \/  u  =  v )  <->  E. x  E. y ( x  =  u  /\  y  =  v ) )
qed:25,26:  |-  ( ( -.  A. x x  =  y  \/  u  =  v )  ->  ( [ u  /  x ] [ v  /  y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) )
 |-  (
 ( -.  A. x  x  =  y  \/  u  =  v )  ->  ( [ u  /  x ] [ v  /  y ] ph  <->  E. x E. y
 ( ( x  =  u  /\  y  =  v )  /\  ph )
 ) )
 
Theorem2uasbanhVD 27820* The following User's Proof is a Virtual Deduction proof (see: wvd1 27473) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh 27463 is 2uasbanhVD 27820 without virtual deductions and was automatically derived from 2uasbanhVD 27820. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
h1::  |-  ( ch  <->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
100:1:  |-  ( ch  ->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
2:100:  |-  (. ch  ->.  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) ).
3:2:  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
4:3:  |-  (. ch  ->.  E. x E. y ( x  =  u  /\  y  =  v  ) ).
5:4:  |-  (. ch  ->.  ( -.  A. x x  =  y  \/  u  =  v )  ).
6:5:  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ph  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) ) ).
7:3,6:  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ph ).
8:2:  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ).
9:5:  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ps  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) ) ).
10:8,9:  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ps ).
101::  |-  ( [ v  /  y ] ( ph  /\  ps )  <->  ( [ v  /  y ] ph  /\  [ v  /  y ] ps ) )
102:101:  |-  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  [ u  /  x ] ( [ v  /  y ] ph  /\  [ v  /  y ] ps ) )
103::  |-  ( [ u  /  x ] ( [ v  /  y ] ph  /\  [ v  /  y  ] ps )  <->  ( [ u  /  x ] [ v  /  y ] ph  /\  [ u  /  x ] [ v  /  y ] ps ) )
104:102,103:  |-  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  ( [ u  /  x ] [ v  /  y ] ph  /\  [ u  /  x ] [ v  /  y ] ps ) )
11:7,10,104:  |-  (. ch  ->.  [ u  /  x ] [ v  /  y ] ( ph  /\  ps ) ).
110:5:  |-  (. ch  ->.  ( [ u  /  x ] [ v  /  y ] ( ph  /\  ps )  <->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) ) ).
12:11,110:  |-  (. ch  ->.  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) ).
120:12:  |-  ( ch  ->  E. x E. y ( ( x  =  u  /\  y  =  v  )  /\  ( ph  /\  ps ) ) )
13:1,120:  |-  ( ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) )
14::  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) ) ).
15:14:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( x  =  u  /\  y  =  v ) ).
16:14:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( ph  /\  ps ) ).
17:16:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ph ).
18:15,17:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ph ) ).
19:18:  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->  ( ( x  =  u  /\  y  =  v )  /\  ph ) )
20:19:  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) )  ->  E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) )
21:20:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  (  ph  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph ) )
22:16:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ps ).
23:15,22:  |-  (. ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->.  ( ( x  =  u  /\  y  =  v )  /\  ps ) ).
24:23:  |-  ( ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps  ) )  ->  ( ( x  =  u  /\  y  =  v )  /\  ps ) )
25:24:  |-  ( E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) )  ->  E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )
26:25:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  (  ph  /\  ps ) )  ->  E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ps ) )
27:21,26:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  (  ph  /\  ps ) )  ->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y (  ( x  =  u  /\  y  =  v )  /\  ps ) ) )
qed:13,27:  |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  (  ph  /\  ps ) )  <->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y (  ( x  =  u  /\  y  =  v )  /\  ps ) ) )
 |-  ( ch 
 <->  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y
 ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )   =>    |-  ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ( ph  /\  ps ) )  <-> 
 ( E. x E. y ( ( x  =  u  /\  y  =  v )  /\  ph )  /\  E. x E. y
 ( ( x  =  u  /\  y  =  v )  /\  ps ) ) )
 
Theoreme2ebindVD 27821 The following User's Proof is a Virtual Deduction proof (see: wvd1 27473) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. e2ebind 27465 is e2ebindVD 27821 without virtual deductions and was automatically derived from e2ebindVD 27821
1::  |-  ( ph  <->  ph )
2:1:  |-  ( A. y y  =  x  ->  ( ph  <->  ph ) )
3:2:  |-  ( A. y y  =  x  ->  ( E. y ph  <->  E. x ph  ) )
4::  |-  (. A. y y  =  x  ->.  A. y y  =  x ).
5:3,4:  |-  (. A. y y  =  x  ->.  ( E. y ph  <->  E. x  ph ) ).
6::  |-  ( A. y y  =  x  ->  A. y A. y y  =  x )
7:5,6:  |-  (. A. y y  =  x  ->.  A. y ( E. y ph  <->  E. x ph ) ).
8:7:  |-  (. A. y y  =  x  ->.  ( E. y E. y ph  <->  E. y E. x ph ) ).
9::  |-  ( E. y E. x ph  <->  E. x E. y ph )
10:8,9:  |-  (. A. y y  =  x  ->.  ( E. y E. y ph  <->  E. x E. y ph ) ).
11::  |-  ( E. y ph  ->  A. y E. y ph )
12:11:  |-  ( E. y E. y ph  <->  E. y ph )
13:10,12:  |-  (. A. y y  =  x  ->.  ( E. x E. y ph  <->  E. y ph ) ).
14:13:  |-  ( A. y y  =  x  ->  ( E. x E. y ph  <->  E.  y ph ) )
15::  |-  ( A. y y  =  x  <->  A. x x  =  y )
qed:14,15:  |-  ( A. x x  =  y  ->  ( E. x E. y ph  <->  E.  y ph ) )
(Contributed by Alan Sare, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x  x  =  y  ->  ( E. x E. y ph  <->  E. y ph )
 )
 
18.23.6  Virtual Deduction transcriptions of textbook proofs
 
Theoremsb5ALTVD 27822* The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 20 Excercise 3.a., which is sb5 1994, found in the "Answers to Starred Exercises" on page 457 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted as a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sb5ALT 27424 is sb5ALTVD 27822 without virtual deductions and was automatically derived from sb5ALTVD 27822.
1::  |-  (. [ y  /  x ] ph  ->.  [ y  /  x ] ph ).
2::  |-  [ y  /  x ] x  =  y
3:1,2:  |-  (. [ y  /  x ] ph  ->.  [ y  /  x ] ( x  =  y  /\  ph ) ).
4:3:  |-  (. [ y  /  x ] ph  ->.  E. x ( x  =  y  /\  ph  ) ).
5:4:  |-  ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph )  )
6::  |-  (. E. x ( x  =  y  /\  ph )  ->.  E. x ( x  =  y  /\  ph ) ).
7::  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph  )  ->.  ( x  =  y  /\  ph ) ).
8:7:  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph  )  ->.  ph ).
9:7:  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph  )  ->.  x  =  y ).
10:8,9:  |-  (. E. x ( x  =  y  /\  ph ) ,. ( x  =  y  /\  ph  )  ->.  [ y  /  x ] ph ).
101::  |-  ( [ y  /  x ] ph  ->  A. x [ y  /  x ] ph )
11:101,10:  |-  ( E. x ( x  =  y  /\  ph )  ->  [ y  /  x ] ph  )
12:5,11:  |-  ( ( [ y  /  x ] ph  ->  E. x ( x  =  y  /\  ph  ) )  /\  ( E. x ( x  =  y  /\  ph )  ->  [ y  /  x ] ph ) )
qed:12:  |-  ( [ y  /  x ] ph  <->  E. x ( x  =  y  /\  ph )  )
(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( [ y  /  x ] ph  <->  E. x ( x  =  y  /\  ph )
 )
 
Theoremvk15.4jVD 27823 The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 15 Excercise 4.f. found in the "Answers to Starred Exercises" on page 442 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. vk15.4j 27427 is vk15.4jVD 27823 without virtual deductions and was automatically derived from vk15.4jVD 27823. Step numbers greater than 25 are additional steps necessary for the sequent calculus proof not contained in the Fitch-style proof. Otherwise, step i of the User's Proof corresponds to step i of the Fitch-style proof.
h1::  |-  -.  ( E. x -.  ph  /\  E. x ( ps  /\  -.  ch ) )
h2::  |-  ( A. x ch  ->  -.  E. x ( th  /\  ta  ) )
h3::  |-  -.  A. x ( ta  ->  ph )
4::  |-  (. -.  E. x -.  th  ->.  -.  E. x -.  th ).
5:4:  |-  (. -.  E. x -.  th  ->.  A. x th ).
6:3:  |-  E. x ( ta  /\  -.  ph )
7::  |-  (. -.  E. x -.  th ,. ( ta  /\  -.  ph )  ->.  ( ta  /\  -.  ph ) ).
8:7:  |-  (. -.  E. x -.  th ,. ( ta  /\  -.  ph )  ->.  ta ).
9:7:  |-  (. -.  E. x -.  th ,. ( ta  /\  -.  ph )  ->.  -.  ph ).
10:5:  |-  (. -.  E. x -.  th  ->.  th ).
11:10,8:  |-  (. -.  E. x -.  th ,. ( ta  /\  -.  ph )  ->.  ( th  /\  ta ) ).
12:11:  |-  (. -.  E. x -.  th ,. ( ta  /\  -.  ph )  ->.  E. x ( th  /\  ta ) ).
13:12:  |-  (. -.  E. x -.  th ,. ( ta  /\  -.  ph )  ->.  -.  -.  E. x ( th  /\  ta ) ).
14:2,13:  |-  (. -.  E. x -.  th ,. ( ta  /\  -.  ph )  ->.  -.  A. x ch ).
140::  |-  ( E. x -.  th  ->  A. x E. x -.  th  )
141:140:  |-  ( -.  E. x -.  th  ->  A. x -.  E. x  -.  th )
142::  |-  ( A. x ch  ->  A. x A. x ch )
143:142:  |-  ( -.  A. x ch  ->  A. x -.  A. x ch  )
144:6,14,141,143:  |-  (. -.  E. x -.  th  ->.  -.  A. x ch  ).
15:1:  |-  ( -.  E. x -.  ph  \/  -.  E. x ( ps  /\  -.  ch ) )
16:9:  |-  (. -.  E. x -.  th ,. ( ta  /\  -.  ph )  ->.  E. x -.  ph ).
161::  |-  ( E. x -.  ph  ->  A. x E. x -.  ph  )
162:6,16,141,161:  |-  (. -.  E. x -.  th  ->.  E. x -.  ph  ).
17:162:  |-  (. -.  E. x -.  th  ->.  -.  -.  E. x  -.  ph ).
18:15,17:  |-  (. -.  E. x -.  th  ->.  -.  E. x (  ps  /\  -.  ch ) ).
19:18:  |-  (. -.  E. x -.  th  ->.  A. x ( ps  ->  ch ) ).
20:144:  |-  (. -.  E. x -.  th  ->.  E. x -.  ch  ).
21::  |-  (. -.  E. x -.  th ,. -.  ch  ->.  -.  ch ).
22:19:  |-  (. -.  E. x -.  th  ->.  ( ps  ->  ch  ) ).
23:21,22:  |-  (. -.  E. x -.  th ,. -.  ch  ->.  -.  ps ).
24:23:  |-  (. -.  E. x -.  th ,. -.  ch  ->.  E.  x -.  ps ).
240::  |-  ( E. x -.  ps  ->  A. x E. x -.  ps  )
241:20,24,141,240:  |-  (. -.  E. x -.  th  ->.  E. x -.  ps  ).
25:241:  |-  (. -.  E. x -.  th  ->.  -.  A. x ps  ).
qed:25:  |-  ( -.  E. x -.  th  ->  -.  A. x ps )
(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  -.  ( E. x  -.  ph  /\ 
 E. x ( ps 
 /\  -.  ch )
 )   &    |-  ( A. x ch  ->  -.  E. x ( th  /\  ta )
 )   &    |- 
 -.  A. x ( ta 
 ->  ph )   =>    |-  ( -.  E. x  -.  th  ->  -.  A. x ps )
 
Theoremnotnot2ALTVD 27824 The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Theorem 5 of Section 14 of [Margaris] p. 59 ( which is notnot2 106). The same proof may also be interpreted as a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. notnot2ALT 27428 is notnot2ALTVD 27824 without virtual deductions and was automatically derived from notnot2ALTVD 27824. Step i of the User's Proof corresponds to step i of the Fitch-style proof.
1::  |-  (. -.  -.  ph  ->.  -.  -.  ph ).
2::  |-  ( -.  -.  ph  ->  ( -.  ph  ->  -.  -.  -.  ph ) )
3:1:  |-  (. -.  -.  ph  ->.  ( -.  ph  ->  -.  -.  -.  ph ) ).
4::  |-  ( ( -.  ph  ->  -.  -.  -.  ph )  ->  ( -.  -.  ph  ->  ph ) )
5:3:  |-  (. -.  -.  ph  ->.  ( -.  -.  ph  ->  ph ) ).
6:5,1:  |-  (. -.  -.  ph  ->.  ph ).
qed:6:  |-  ( -.  -.  ph  ->  ph )
(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( -.  -.  ph  ->  ph )
 
Theoremcon3ALTVD 27825 The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Theorem 7 of Section 14 of [Margaris] p. 60 ( which is con3 128). The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. con3ALT 27429 is con3ALTVD 27825 without virtual deductions and was automatically derived from con3ALTVD 27825. Step i of the User's Proof corresponds to step i of the Fitch-style proof.
1::  |-  (. ( ph  ->  ps )  ->.  ( ph  ->  ps ) ).
2::  |-  (. ( ph  ->  ps ) ,. -.  -.  ph  ->.  -.  -.  ph ).
3::  |-  ( -.  -.  ph  ->  ph )
4:2:  |-  (. ( ph  ->  ps ) ,. -.  -.  ph  ->.  ph ).
5:1,4:  |-  (. ( ph  ->  ps ) ,. -.  -.  ph  ->.  ps ).
6::  |-  ( ps  ->  -.  -.  ps )
7:6,5:  |-  (. ( ph  ->  ps ) ,. -.  -.  ph  ->.  -.  -.  ps ).
8:7:  |-  (. ( ph  ->  ps )  ->.  ( -.  -.  ph  ->  -.  -.  ps  ) ).
9::  |-  ( ( -.  -.  ph  ->  -.  -.  ps )  ->  ( -.  ps  ->  -.  ph ) )
10:8:  |-  (. ( ph  ->  ps )