HomeHome Metamath Proof Explorer
Theorem List (p. 342 of 386)
< 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-26036)
  Hilbert Space Explorer  Hilbert Space Explorer
(26037-27561)
  Users' Mathboxes  Users' Mathboxes
(27562-38521)
 

Theorem List for Metamath Proof Explorer - 34101-34200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
TheoremtrintALT 34101* The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 34101 is an alternative proof of trint 4547. trintALT 34101 is trintALTVD 34100 without virtual deductions and was automatically derived from trintALTVD 34100 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
 
Theoremundif3VD 34102 The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3756. 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. undif3 3756 is undif3VD 34102 without virtual deductions and was automatically derived from undif3VD 34102.
1::  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  x  e.  ( B  \  C ) ) )
2::  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
3:2:  |-  ( ( x  e.  A  \/  x  e.  ( B  \  C ) )  <->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
4:1,3:  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
5::  |-  (. x  e.  A  ->.  x  e.  A ).
6:5:  |-  (. x  e.  A  ->.  ( x  e.  A  \/  x  e.  B ) ).
7:5:  |-  (. x  e.  A  ->.  ( -.  x  e.  C  \/  x  e.  A ) ).
8:6,7:  |-  (. x  e.  A  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) ).
9:8:  |-  ( x  e.  A  ->  ( ( x  e.  A  \/  x  e.  B )  /\  (  -.  x  e.  C  \/  x  e.  A ) ) )
10::  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( x  e.  B  /\  -.  x  e.  C ) ).
11:10:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  x  e.  B ).
12:10:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  -.  x  e.  C  ).
13:11:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( x  e.  A  \/  x  e.  B ) ).
14:12:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( -.  x  e.  C  \/  x  e.  A ) ).
15:13,14:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) ).
16:15:  |-  ( ( x  e.  B  /\  -.  x  e.  C )  ->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
17:9,16:  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) )  ->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
18::  |-  (. ( x  e.  A  /\  -.  x  e.  C )  ->.  ( x  e.  A  /\  -.  x  e.  C ) ).
19:18:  |-  (. ( x  e.  A  /\  -.  x  e.  C )  ->.  x  e.  A ).
20:18:  |-  (. ( x  e.  A  /\  -.  x  e.  C )  ->.  -.  x  e.  C  ).
21:18:  |-  (. ( x  e.  A  /\  -.  x  e.  C )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) ).
22:21:  |-  ( ( x  e.  A  /\  -.  x  e.  C )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
23::  |-  (. ( x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  /\  x  e.  A ) ).
24:23:  |-  (. ( x  e.  A  /\  x  e.  A )  ->.  x  e.  A ).
25:24:  |-  (. ( x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) ).
26:25:  |-  ( ( x  e.  A  /\  x  e.  A )  ->  ( x  e.  A  \/  (  x  e.  B  /\  -.  x  e.  C ) ) )
27:10:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) ).
28:27:  |-  ( ( x  e.  B  /\  -.  x  e.  C )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
29::  |-  (. ( x  e.  B  /\  x  e.  A )  ->.  ( x  e.  B  /\  x  e.  A ) ).
30:29:  |-  (. ( x  e.  B  /\  x  e.  A )  ->.  x  e.  A ).
31:30:  |-  (. ( x  e.  B  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) ).
32:31:  |-  ( ( x  e.  B  /\  x  e.  A )  ->  ( x  e.  A  \/  (  x  e.  B  /\  -.  x  e.  C ) ) )
33:22,26:  |-  ( ( ( x  e.  A  /\  -.  x  e.  C )  \/  ( x  e.  A  /\  x  e.  A ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
34:28,32:  |-  ( ( ( x  e.  B  /\  -.  x  e.  C )  \/  ( x  e.  B  /\  x  e.  A ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
35:33,34:  |-  ( ( ( ( x  e.  A  /\  -.  x  e.  C )  \/  ( x  e.  A  /\  x  e.  A ) )  \/  ( ( x  e.  B  /\  -.  x  e.  C )  \/  ( x  e.  B  /\  x  e.  A ) ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
36::  |-  ( ( ( ( x  e.  A  /\  -.  x  e.  C )  \/  ( x  e.  A  /\  x  e.  A ) )  \/  ( ( x  e.  B  /\  -.  x  e.  C )  \/  ( x  e.  B  /\  x  e.  A ) ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
37:36,35:  |-  ( ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
38:17,37:  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
39::  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
40:39:  |-  ( -.  x  e.  ( C  \  A )  <->  -.  ( x  e.  C  /\  -.  x  e.  A ) )
41::  |-  ( -.  ( x  e.  C  /\  -.  x  e.  A )  <->  ( -.  x  e.  C  \/  x  e.  A ) )
42:40,41:  |-  ( -.  x  e.  ( C  \  A )  <->  ( -.  x  e.  C  \/  x  e.  A ) )
43::  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B  ) )
44:43,42:  |-  ( ( x  e.  ( A  u.  B )  /\  -.  x  e.  ( C  \  A )  )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  /\  x  e.  A ) ) )
45::  |-  ( x  e.  ( ( A  u.  B )  \  ( C  \  A ) )  <->  (  x  e.  ( A  u.  B )  /\  -.  x  e.  ( C  \  A ) ) )
46:45,44:  |-  ( x  e.  ( ( A  u.  B )  \  ( C  \  A ) )  <->  (  ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
47:4,38:  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
48:46,47:  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  x  e.  ( ( A  u.  B )  \  ( C  \  A ) ) )
49:48:  |-  A. x ( x  e.  ( A  u.  ( B  \  C ) )  <->  x  e.  ( ( A  u.  B )  \  ( C  \  A ) ) )
qed:49:  |-  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B )  \  ( C  \  A ) )
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B )  \  ( C 
 \  A ) )
 
TheoremsbcssgVD 34103 Virtual deduction proof of sbcssg 3928. 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. sbcssg 3928 is sbcssgVD 34103 without virtual deductions and was automatically derived from sbcssgVD 34103.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) ).
3:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) ).
4:2,3:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. y  e.  C  ->  [. A  /  x ]. y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D  ) ) ).
5:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  ( [. A  /  x ]. y  e.  C  ->  [. A  /  x ]. y  e.  D ) ) ).
6:4,5:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D ) ) ).
7:6:  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D ) ) ).
8:7:  |-  (. A  e.  B  ->.  ( A. y [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  A. y ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D )  ) ).
9:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( y  e.  C  ->  y  e.  D )  <->  A. y [. A  /  x ]. ( y  e.  C  ->  y  e.  D ) ) ).
10:8,9:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( y  e.  C  ->  y  e.  D )  <->  A. y ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D )  ) ).
11::  |-  ( C  C_  D  <->  A. y ( y  e.  C  ->  y  e.  D ) )
110:11:  |-  A. x ( C  C_  D  <->  A. y ( y  e.  C  ->  y  e.  D ) )
12:1,110:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. C  C_  D  <->  [. A  /  x ]. A. y ( y  e.  C  ->  y  e.  D ) ) ).
13:10,12:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. C  C_  D  <->  A. y ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D ) ) ).
14::  |-  ( [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D  <->  A.  y ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D ) )
15:13,14:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. C  C_  D  <->  [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D ) ).
qed:15:  |-  ( A  e.  B  ->  ( [. A  /  x ]. C  C_  D  <->  [_  A  /  x ]_ C  C_  [_ A  /  x ]_ D ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 [. A  /  x ]. C  C_  D  <->  [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D ) )
 
TheoremcsbingVD 34104 Virtual deduction proof of csbingOLD 34038. 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. csbingOLD 34038 is csbingVD 34104 without virtual deductions and was automatically derived from csbingVD 34104.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2::  |-  ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D )  }
20:2:  |-  A. x ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
30:1,20:  |-  (. A  e.  B  ->.  [. A  /  x ]. ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) } ).
3:1,30:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) } ).
4:1:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
5:3,4:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
6:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) ).
7:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) ).
8:6,7:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D )  ) ).
9:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) ).
10:9,8:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
11:10:  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
12:11:  |-  (. A  e.  B  ->.  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) }  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
13:5,12:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
14::  |-  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  =  {  y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }
15:13,14:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) ).
qed:15:  |-  ( A  e.  B  ->  [_ A  /  x ]_ ( C  i^i  D )  =  (  [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) )
 
TheoremonfrALTlem5VD 34105* Virtual deduction proof of onfrALTlem5 33727. 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. onfrALTlem5 33727 is onfrALTlem5VD 34105 without virtual deductions and was automatically derived from onfrALTlem5VD 34105.
1::  |-  a  e.  _V
2:1:  |-  ( a  i^i  x )  e.  _V
3:2:  |-  ( [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) )
4:3:  |-  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  -.  ( a  i^i  x )  =  (/) )
5::  |-  ( ( a  i^i  x )  =/=  (/)  <->  -.  ( a  i^i  x  )  =  (/) )
6:4,5:  |-  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =/=  (/) )
7:2:  |-  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  /  b ]. -.  b  =  (/) )
8::  |-  ( b  =/=  (/)  <->  -.  b  =  (/) )
9:8:  |-  A. b ( b  =/=  (/)  <->  -.  b  =  (/) )
10:2,9:  |-  ( [. ( a  i^i  x )  /  b ]. b  =/=  (/)  <->  [. ( a  i^i  x )  /  b ]. -.  b  =  (/) )
11:7,10:  |-  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  /  b ]. b  =/=  (/) )
12:6,11:  |-  ( [. ( a  i^i  x )  /  b ]. b  =/=  (/)  <->  (  a  i^i  x )  =/=  (/) )
13:2:  |-  ( [. ( a  i^i  x )  /  b ]. b  C_  ( a  i^i  x  )  <->  ( a  i^i  x )  C_  ( a  i^i  x ) )
14:12,13:  |-  ( ( [. ( a  i^i  x )  /  b ]. b  C_  ( a  i^i  x )  /\  [. ( a  i^i  x )  /  b ]. b  =/=  (/) )  <->  ( ( a  i^i  x )  C_  ( a  i^i  x )  /\  ( a  i^i  x )  =/=  (/) ) )
15:2:  |-  ( [. ( a  i^i  x )  /  b ]. ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  <->  ( [. ( a  i^i  x )  /  b ]. b  C_  ( a  i^i  x )  /\  [. ( a  i^i  x )  /  b ]. b  =/=  (/) ) )
16:15,14:  |-  ( [. ( a  i^i  x )  /  b ]. ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  <->  ( ( a  i^i  x )  C_  ( a  i^i  x )  /\  ( a  i^i  x )  =/=  (/) ) )
17:2:  |-  [_ ( a  i^i  x )  /  b ]_ ( b  i^i  y )  =  (  [_ ( a  i^i  x )  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )
18:2:  |-  [_ ( a  i^i  x )  /  b ]_ b  =  ( a  i^i  x )
19:2:  |-  [_ ( a  i^i  x )  /  b ]_ y  =  y
20:18,19:  |-  ( [_ ( a  i^i  x )  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )  =  ( ( a  i^i  x )  i^i  y )
21:17,20:  |-  [_ ( a  i^i  x )  /  b ]_ ( b  i^i  y )  =  ( (  a  i^i  x )  i^i  y )
22:2:  |-  ( [. ( a  i^i  x )  /  b ]. ( b  i^i  y )  =  (/)  <->  [_ ( a  i^i  x )  /  b ]_ ( b  i^i  y )  =  [_ ( a  i^i  x )  /  b ]_  (/) )
23:2:  |-  [_ ( a  i^i  x )  /  b ]_ (/)  =  (/)
24:21,23:  |-  ( [_ ( a  i^i  x )  /  b ]_ ( b  i^i  y )  =  [_ ( a  i^i  x )  /  b ]_ (/)  <->  ( ( a  i^i  x )  i^i  y )  =  (/) )
25:22,24:  |-  ( [. ( a  i^i  x )  /  b ]. ( b  i^i  y )  =  (/)  <->  ( ( a  i^i  x )  i^i  y )  =  (/) )
26:2:  |-  ( [. ( a  i^i  x )  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x ) )
27:25,26:  |-  ( ( [. ( a  i^i  x )  /  b ]. y  e.  b  /\  [.  ( a  i^i  x )  /  b ]. ( b  i^i  y )  =  (/) )  <->  ( y  e.  ( a  i^i  x )  /\  ( (  a  i^i  x )  i^i  y )  =  (/) ) )
28:2:  |-  ( [. ( a  i^i  x )  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  ( [. ( a  i^i  x )  /  b ]. y  e.  b  /\  [. ( a  i^i  x )  /  b ]. ( b  i^i  y )  =  (/) ) )
29:27,28:  |-  ( [. ( a  i^i  x )  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) ) )
30:29:  |-  A. y ( [. ( a  i^i  x )  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) ) )
31:30:  |-  ( E. y [. ( a  i^i  x )  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  E. y ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) ) )
32::  |-  ( E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y )  =  (/)  <->  E. y ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/)  ) )
33:31,32:  |-  ( E. y [. ( a  i^i  x )  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y )  =  (/) )
34:2:  |-  ( E. y [. ( a  i^i  x )  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  [. ( a  i^i  x )  /  b ]. E. y ( y  e.  b  /\  (  b  i^i  y )  =  (/) ) )
35:33,34:  |-  ( [. ( a  i^i  x )  /  b ]. E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y  )  =  (/) )
36::  |-  ( E. y  e.  b ( b  i^i  y )  =  (/)  <->  E. y  ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
37:36:  |-  A. b ( E. y  e.  b ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
38:2,37:  |-  ( [. ( a  i^i  x )  /  b ]. E. y  e.  b ( b  i^i  y )  =  (/)  <->  [. ( a  i^i  x )  /  b ]. E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
39:35,38:  |-  ( [. ( a  i^i  x )  /  b ]. E. y  e.  b ( b  i^i  y )  =  (/)  <->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y )  =  (/) )
40:16,39:  |-  ( ( [. ( a  i^i  x )  /  b ]. ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  ->  [. ( a  i^i  x )  /  b ]. E. y  e.  b ( b  i^i  y )  =  (/) )  <->  ( ( ( a  i^i  x )  C_  ( a  i^i  x )  /\  ( a  i^i  x )  =/=  (/) )  ->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y )  =  (/) ) )
41:2:  |-  ( [. ( a  i^i  x )  /  b ]. ( ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  ->  E. y  e.  b ( b  i^i  y )  =  (/) )  <->  ( [. ( a  i^i  x )  /  b ]. ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  ->  [. ( a  i^i  x )  /  b ]. E. y  e.  b ( b  i^i  y )  =  (/) ) )
qed:40,41:  |-  ( [. ( a  i^i  x )  /  b ]. ( ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  ->  E. y  e.  b ( b  i^i  y )  =  (/) )  <->  ( ( ( a  i^i  x )  C_  ( a  i^i  x )  /\  ( a  i^i  x )  =/=  (/) )  ->  E. y  e.  ( a  i^i  x  ) ( ( a  i^i  x )  i^i  y )  =  (/) ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( [. ( a  i^i  x )  /  b ]. (
 ( b  C_  (
 a  i^i  x )  /\  b  =/=  (/) )  ->  E. y  e.  b  ( b  i^i  y )  =  (/) )  <->  ( ( ( a  i^i  x ) 
 C_  ( a  i^i 
 x )  /\  (
 a  i^i  x )  =/= 
 (/) )  ->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y )  =  (/) ) )
 
TheoremonfrALTlem4VD 34106* Virtual deduction proof of onfrALTlem4 33728. 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. onfrALTlem4 33728 is onfrALTlem4VD 34106 without virtual deductions and was automatically derived from onfrALTlem4VD 34106.
1::  |-  y  e.  _V
2:1:  |-  ( [. y  /  x ]. ( a  i^i  x )  =  (/)  <->  [_  y  /  x ]_ ( a  i^i  x )  =  [_ y  /  x ]_ (/) )
3:1:  |-  [_ y  /  x ]_ ( a  i^i  x )  =  ( [_ y  /  x ]_  a  i^i  [_ y  /  x ]_ x )
4:1:  |-  [_ y  /  x ]_ a  =  a
5:1:  |-  [_ y  /  x ]_ x  =  y
6:4,5:  |-  ( [_ y  /  x ]_ a  i^i  [_ y  /  x ]_ x )  =  (  a  i^i  y )
7:3,6:  |-  [_ y  /  x ]_ ( a  i^i  x )  =  ( a  i^i  y )
8:1:  |-  [_ y  /  x ]_ (/)  =  (/)
9:7,8:  |-  ( [_ y  /  x ]_ ( a  i^i  x )  =  [_ y  /  x ]_  (/)  <->  ( a  i^i  y )  =  (/) )
10:2,9:  |-  ( [. y  /  x ]. ( a  i^i  x )  =  (/)  <->  ( a  i^i  y )  =  (/) )
11:1:  |-  ( [. y  /  x ]. x  e.  a  <->  y  e.  a )
12:11,10:  |-  ( ( [. y  /  x ]. x  e.  a  /\  [. y  /  x ]. (  a  i^i  x )  =  (/) )  <->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
13:1:  |-  ( [. y  /  x ]. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  ( [. y  /  x ]. x  e.  a  /\  [. y  /  x ]. ( a  i^i  x )  =  (/) ) )
qed:13,12:  |-  ( [. y  /  x ]. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( [. y  /  x ]. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
 
TheoremonfrALTlem3VD 34107* Virtual deduction proof of onfrALTlem3 33729. 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. onfrALTlem3 33729 is onfrALTlem3VD 34107 without virtual deductions and was automatically derived from onfrALTlem3VD 34107.
1::  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  ( a  C_  On  /\  a  =/=  (/) ) ).
2::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ).
3:2:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  x  e.  a ).
4:1:  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  a  C_  On ).
5:3,4:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  x  e.  On ).
6:5:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  Ord  x ).
7:6:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  _E  We  x ).
8::  |-  ( a  i^i  x )  C_  x
9:7,8:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  _E  We  ( a  i^i  x ) ).
10:9:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  _E  Fr  ( a  i^i  x ) ).
11:10:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  A. b ( ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  ->  E. y  e.  b ( b  i^i  y )  =  (/) ) ).
12::  |-  x  e.  _V
13:12,8:  |-  ( a  i^i  x )  e.  _V
14:13,11:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  [. ( a  i^i  x )  /  b ]. ( ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  ->  E. y  e.  b ( b  i^i  y )  =  (/) ) ).
15::  |-  ( [. ( a  i^i  x )  /  b ]. ( ( b  C_  ( a  i^i  x )  /\  b  =/=  (/) )  ->  E. y  e.  b ( b  i^i  y )  =  (/) )  <->  ( ( ( a  i^i  x )  C_  ( a  i^i  x )  /\  ( a  i^i  x )  =/=  (/) )  ->  E. y  e.  ( a  i^i  x ) (  ( a  i^i  x )  i^i  y )  =  (/) ) )
16:14,15:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  ( ( ( a  i^i  x )  C_  ( a  i^i  x )  /\  (  a  i^i  x )  =/=  (/) )  ->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y )  =  (/) ) ).
17::  |-  ( a  i^i  x )  C_  ( a  i^i  x )
18:2:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  -.  ( a  i^i  x )  =  (/) ).
19:18:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  ( a  i^i  x )  =/=  (/) ).
20:17,19:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  ( ( a  i^i  x )  C_  ( a  i^i  x )  /\  ( a  i^i  x )  =/=  (/) ) ).
qed:16,20:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y  )  =  (/) ).
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (. (
 a  C_  On  /\  a  =/= 
 (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y )  =  (/) ).
 
Theoremsimplbi2comtVD 34108 Virtual deduction proof of simplbi2comt 624. 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. simplbi2comt 624 is simplbi2comtVD 34108 without virtual deductions and was automatically derived from simplbi2comtVD 34108.
1::  |-  (. ( ph  <->  ( ps  /\  ch ) )  ->.  ( ph  <->  (  ps  /\  ch ) ) ).
2:1:  |-  (. ( ph  <->  ( ps  /\  ch ) )  ->.  ( ( ps  /\  ch  )  ->  ph ) ).
3:2:  |-  (. ( ph  <->  ( ps  /\  ch ) )  ->.  ( ps  ->  ( ch  ->  ph ) ) ).
4:3:  |-  (. ( ph  <->  ( ps  /\  ch ) )  ->.  ( ch  ->  ( ps  ->  ph ) ) ).
qed:4:  |-  ( ( ph  <->  ( ps  /\  ch ) )  ->  ( ch  ->  ( ps  ->  ph ) ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  <->  ( ps  /\  ch ) )  ->  ( ch  ->  ( ps  ->  ph ) ) )
 
TheoremonfrALTlem2VD 34109* Virtual deduction proof of onfrALTlem2 33731. 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. onfrALTlem2 33731 is onfrALTlem2VD 34109 without virtual deductions and was automatically derived from onfrALTlem2VD 34109.
1::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) ) ).
2:1:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  z  e.  ( a  i^i  y ) ).
3:2:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  z  e.  a ).
4::  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  ( a  C_  On  /\  a  =/=  (/) ) ).
5::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ).
6:5:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  x  e.  a ).
7:4:  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  a  C_  On ).
8:6,7:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  x  e.  On ).
9:8:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  Ord  x ).
10:9:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  Tr  x ).
11:1:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  y  e.  ( a  i^i  x ) ).
12:11:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  y  e.  x ).
13:2:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  z  e.  y ).
14:10,12,13:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  z  e.  x ).
15:3,14:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  z  e.  ( a  i^i  x ) ).
16:13,15:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  /\  z  e.  ( a  i^i  y ) )  ->.  z  e.  ( ( a  i^i  x )  i^i  y ) ).
17:16:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  ( z  e.  ( a  i^i  y )  ->  z  e.  ( ( a  i^i  x )  i^i  y ) ) ).
18:17:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  A. z ( z  e.  ( a  i^i  y )  ->  z  e.  ( ( a  i^i  x )  i^i  y ) ) ).
19:18:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  ( a  i^i  y )  C_  ( ( a  i^i  x )  i^i  y ) ).
20::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) ) ).
21:20:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  ( ( a  i^i  x )  i^i  y )  =  (/) ).
22:19,21:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  ( a  i^i  y )  =  (/) ).
23:20:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  y  e.  ( a  i^i  x ) ).
24:23:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  y  e.  a ).
25:22,24:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) ) ,  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y  )  =  (/) )  ->.  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ).
26:25:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) )  ->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ) ).
27:26:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  A. y ( ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x  )  i^i  y )  =  (/) )  ->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ) ).
28:27:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  ( E. y ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x  )  i^i  y )  =  (/) )  ->  E. y ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ) ).
29::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y  )  =  (/) ).
30:29:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  E. y ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) ) ).
31:28,30:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  E. y ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ).
qed:31:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  a ( a  i^i  y )  =  (/) ).
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (. (
 a  C_  On  /\  a  =/= 
 (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  a  ( a  i^i  y )  =  (/) ).
 
TheoremonfrALTlem1VD 34110* Virtual deduction proof of onfrALTlem1 33733. 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. onfrALTlem1 33733 is onfrALTlem1VD 34110 without virtual deductions and was automatically derived from onfrALTlem1VD 34110.
1::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  ( x  e.  a  /\  ( a  i^i  x )  =  (/) ) ).
2:1:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. x ( x  e.  a  /\  ( a  i^i  x )  =  (/) ) ).
3:2:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. y [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ).
4::  |-  ( [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/)  )  <->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
5:4:  |-  A. y ( [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
6:5:  |-  ( E. y [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  E. y ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
7:3,6:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. y ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ).
8::  |-  ( E. y  e.  a ( a  i^i  y )  =  (/)  <->  E. y (  y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
qed:7,8:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  a ( a  i^i  y )  =  (/) ).
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (. (
 a  C_  On  /\  a  =/= 
 (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  a  ( a  i^i  y )  =  (/) ).
 
TheoremonfrALTVD 34111 Virtual deduction proof of onfrALT 33734. 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. onfrALT 33734 is onfrALTVD 34111 without virtual deductions and was automatically derived from onfrALTVD 34111.
1::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  -.  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  a ( a  i^i  y )  =  (/) ).
2::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  a ( a  i^i  y )  =  (/) ).
3:1:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. x  e.  a  ->.  ( -.  ( a  i^i  x )  =  (/)  ->  E. y  e.  a ( a  i^i  y )  =  (/) ) ).
4:2:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. x  e.  a  ->.  ( ( a  i^i  x )  =  (/)  ->  E. y  e.  a ( a  i^i  y )  =  (/) ) ).
5::  |-  ( ( a  i^i  x )  =  (/)  \/  -.  ( a  i^i  x )  =  (/) )
6:5,4,3:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. x  e.  a  ->.  E. y  e.  a ( a  i^i  y )  =  (/) ).
7:6:  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  ( x  e.  a  ->  E. y  e.  a ( a  i^i  y )  =  (/) ) ).
8:7:  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  A. x ( x  e.  a  ->  E. y  e.  a ( a  i^i  y )  =  (/) ) ).
9:8:  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  ( E. x x  e.  a  ->  E. y  e.  a ( a  i^i  y )  =  (/) ) ).
10::  |-  ( a  =/=  (/)  <->  E. x x  e.  a )
11:9,10:  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  ( a  =/=  (/)  ->  E. y  e.  a ( a  i^i  y )  =  (/) ) ).
12::  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  ( a  C_  On  /\  a  =/=  (/) ) ).
13:12:  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  a  =/=  (/) ).
14:13,11:  |-  (. ( a  C_  On  /\  a  =/=  (/) )  ->.  E. y  e.  a ( a  i^i  y )  =  (/) ).
15:14:  |-  ( ( a  C_  On  /\  a  =/=  (/) )  ->  E. y  e.  a  ( a  i^i  y )  =  (/) )
16:15:  |-  A. a ( ( a  C_  On  /\  a  =/=  (/) )  ->  E. y  e.  a ( a  i^i  y )  =  (/) )
qed:16:  |-  _E  Fr  On
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  _E  Fr  On
 
Theoremcsbeq2gVD 34112 Virtual deduction proof of csbeq2gOLD 33735. 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. csbeq2gOLD 33735 is csbeq2gVD 34112 without virtual deductions and was automatically derived from csbeq2gVD 34112.
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 34113 Virtual deduction proof of csbsng 4074. 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. csbsng 4074 is csbsngVD 34113 without virtual deductions and was automatically derived from csbsngVD 34113.
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 34114 Virtual deduction proof of csbxpgOLD 34037. 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. csbxpgOLD 34037 is csbxpgVD 34114 without virtual deductions and was automatically derived from csbxpgVD 34114.
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 34115 Virtual deduction proof of csbresgOLD 34039. 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. csbresgOLD 34039 is csbresgVD 34115 without virtual deductions and was automatically derived from csbresgVD 34115.
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 34116 Virtual deduction proof of csbrngOLD 34040. 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 34040 is csbrngVD 34116 without virtual deductions and was automatically derived from csbrngVD 34116.
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 34117 Virtual deduction proof of csbima12gALTOLD 34041. 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. csbima12gALTOLD 34041 is csbima12gALTVD 34117 without virtual deductions and was automatically derived from csbima12gALTVD 34117.
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 34118 Virtual deduction proof of csbunigOLD 34035. 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. csbunigOLD 34035 is csbunigVD 34118 without virtual deductions and was automatically derived from csbunigVD 34118.
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 34119 Virtual deduction proof of csbfv12gALTOLD 34036. 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. csbfv12gALTOLD 34036 is csbfv12gALTVD 34119 without virtual deductions and was automatically derived from csbfv12gALTVD 34119.
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 34120 Virtual deduction proof of con5 33698. 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. con5 33698 is con5VD 34120 without virtual deductions and was automatically derived from con5VD 34120.
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 34121 Virtual deduction proof of relopab 5117. 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. relopab 5117 is relopabVD 34121 without virtual deductions and was automatically derived from relopabVD 34121.
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 34122 Virtual deduction proof of 19.41rg 33736. 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. 19.41rg 33736 is 19.41rgVD 34122 without virtual deductions and was automatically derived from 19.41rgVD 34122. (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 34123 Virtual deduction proof of 2pm13.193 33738. 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. 2pm13.193 33738 is 2pm13.193VD 34123 without virtual deductions and was automatically derived from 2pm13.193VD 34123. (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  =