HomeHome Metamath Proof Explorer
Theorem List (p. 288 of 323)
< 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-21500)
  Hilbert Space Explorer  Hilbert Space Explorer
(21501-23023)
  Users' Mathboxes  Users' Mathboxes
(23024-32227)
 

Theorem List for Metamath Proof Explorer - 28701-28800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem19.21a3con13vVD 28701* Virtual deduction proof of alrim3con13v 28352. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. ( ph  ->  A. x ph )  ->.  ( ph  ->  A. x ph ) ).
2::  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ( ps  /\  ph  /\  ch ) ).
3:2,?: e2 28465  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ps ).
4:2,?: e2 28465  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ph ).
5:2,?: e2 28465  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ch ).
6:1,4,?: e12 28570  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ph ).
7:3,?: e2 28465  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ps ).
8:5,?: e2 28465  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ch ).
9:7,6,8,?: e222 28470  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ( A. x ps  /\  A. x ph  /\  A. x ch ) ).
10:9,?: e2 28465  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ( ps  /\  ph  /\  ch ) ).
11:10:in2  |-  (. ( ph  ->  A. x ph )  ->.  ( ( ps  /\  ph  /\  ch )  ->  A. x ( ps  /\  ph  /\  ch ) ) ).
qed:11:in1  |-  ( ( ph  ->  A. x ph )  ->  ( ( ps  /\  ph  /\  ch )  ->  A. x ( ps  /\  ph  /\  ch ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  ->  A. x ph )  ->  ( ( ps  /\  ph  /\  ch )  ->  A. x ( ps 
 /\  ph  /\  ch )
 ) )
 
TheoremexbirVD 28702 Virtual deduction proof of exbir 1355. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) )  ->.  ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ).
2::  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,.  ( ph  /\  ps )  ->.  ( ph  /\  ps ) ).
3::  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,.  ( ph  /\  ps ) ,  th  ->.  th ).
5:1,2,?: e12 28570  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( ch  <->  th ) ).
6:3,5,?: e32 28604  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps ) ,  th  ->.  ch ).
7:6:  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( th  ->  ch ) ).
8:7:  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) )  ->.  ( ( ph  /\  ps )  ->  ( th  ->  ch ) ) ).
9:8,?: e1_ 28461  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) )  ->.  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) ).
qed:9:  |-  ( ( ( ph  /\  ps )  ->  ( ch  <->  th ) )  ->  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) ) )
(Contributed by Alan Sare, 13-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps )  ->  ( ch  <->  th ) )  ->  ( ph  ->  ( ps  ->  ( th  ->  ch )
 ) ) )
 
TheoremexbiriVD 28703 Virtual deduction proof of exbiri 605. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1::  |-  ( ( ph  /\  ps )  ->  ( ch  <->  th ) )
2::  |-  (. ph  ->.  ph ).
3::  |-  (. ph ,. ps  ->.  ps ).
4::  |-  (. ph ,. ps ,. th  ->.  th ).
5:2,1,?: e10 28529  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 28576  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 28604  |-  (. ph ,. ps ,. th  ->.  ch ).
8:7:  |-  (. ph ,. ps  ->.  ( th  ->  ch ) ).
9:8:  |-  (. ph  ->.  ( ps  ->  ( th  ->  ch ) ) ).
qed:9:  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps )  ->  ( ch  <->  th ) )   =>    |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
 
Theoremrspsbc2VD 28704* Virtual deduction proof of rspsbc2 28353. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2::  |-  (. A  e.  B ,. C  e.  D  ->.  C  e.  D ).
3::  |-  (. A  e.  B ,. C  e.  D ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  B A. y  e.  D ph ).
4:1,3,?: e13 28594  |-  (. A  e.  B ,. C  e.  D ,. A. x  e.  B  A. y  e.  D ph  ->.  [. A  /  x ]. A. y  e.  D ph ).
5:1,4,?: e13 28594  |-  (. A  e.  B ,. C  e.  D ,. A. x  e.  B  A. y  e.  D ph  ->.  A. y  e.  D [. A  /  x ]. ph ).
6:2,5,?: e23 28601  |-  (. A  e.  B ,. C  e.  D ,. A. x  e.  B  A. y  e.  D ph  ->.  [. C  /  y ]. [. A  /  x ]. ph ).
7:6:  |-  (. A  e.  B ,. C  e.  D  ->.  ( A. x  e.  B  A. y  e.  D ph  ->  [. C  /  y ]. [. A  /  x ]. ph ) ).
8:7:  |-  (. A  e.  B  ->.  ( C  e.  D  ->  ( A. x  e.  B A. y  e.  D ph  ->  [. C  /  y ]. [. A  /  x ]. ph ) ) ).
qed:8:  |-  ( A  e.  B  ->  ( C  e.  D  ->  ( A. x  e.  B A. y  e.  D ph  ->  [. C  /  y ]. [. A  /  x ]. ph ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  ( C  e.  D  ->  (
 A. x  e.  B  A. y  e.  D  ph  -> 
 [. C  /  y ]. [. A  /  x ].
 ph ) ) )
 
Theorem3impexpVD 28705 Virtual deduction proof of 3impexp 1356. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ph  /\  ps  /\  ch )  ->  th ) ).
2::  |-  ( ( ph  /\  ps  /\  ch )  <->  ( ( ph  /\  ps )  /\  ch ) )
3:1,2,?: e10 28529  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ( ph  /\  ps )  /\  ch )  ->  th ) ).
4:3,?: e1_ 28461  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ph  /\  ps )  ->  ( ch  ->  th ) ) ).
5:4,?: e1_ 28461  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) ) ).
6:5:  |-  ( ( ( ph  /\  ps  /\  ch )  ->  th )  ->  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) ) )
7::  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) ) ).
8:7,?: e1_ 28461  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ph  /\  ps )  ->  ( ch  ->  th ) ) ).
9:8,?: e1_ 28461  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ( ph  /\  ps )  /\  ch )  ->  th ) ).
10:2,9,?: e01 28525  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  th ) ).
11:10:  |-  ( ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->  ( ( ph  /\  ps  /\  ch )  ->  th ) )
qed:6,11,?: e00 28614  |-  ( ( ( ph  /\  ps  /\  ch )  ->  th )  <->  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps  /\ 
 ch )  ->  th )  <->  (
 ph  ->  ( ps  ->  ( ch  ->  th )
 ) ) )
 
Theorem3impexpbicomVD 28706 Virtual deduction proof of 3impexpbicom 1357. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) ) ).
2::  |-  ( ( th  <->  ta )  <->  ( ta  <->  th ) )
3:1,2,?: e10 28529  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
4:3,?: e1_ 28461  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) ).
5:4:  |-  ( ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) )
6::  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) ).
7:6,?: e1_ 28461  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
8:7,2,?: e10 28529  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) ) ).
9:8:  |-  ( ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) ) )
qed:5,9,?: e00 28614  |-  ( ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps  /\ 
 ch )  ->  ( th 
 <->  ta ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) )
 
Theorem3impexpbicomiVD 28707 Virtual deduction proof of 3impexpbicomi 1358. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1::  |-  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )
qed:1,?: e0_ 28618  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )   =>    |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )
 
TheoremsbcoreleleqVD 28708* Virtual deduction proof of sbcoreleleq 28354. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2:1,?: e1_ 28461  |-  (. A  e.  B  ->.  ( [. A  /  y ]. x  e.  y  <->  x  e.  A ) ).
3:1,?: e1_ 28461  |-  (. A  e.  B  ->.  ( [. A  /  y ]. y  e.  x  <->  A  e.  x ) ).
4:1,?: e1_ 28461  |-  (. A  e.  B  ->.  ( [. A  /  y ]. x  =  y  <->  x  =  A ) ).
5:2,3,4,?: e111 28508  |-  (. A  e.  B  ->.  ( ( x  e.  A  \/  A  e.  x  \/  x  =  A )  <->  ( [. A  /  y ]. x  e.  y  \/  [. A  /  y ]. y  e.  x  \/  [. A  /  y ]. x  =  y ) ) ).
6:1,?: e1_ 28461  |-  (. A  e.  B  ->.  ( [. A  /  y ]. ( x  e.  y  \/  y  e.  x  \/  x  =  y )  <->  ( [. A  /  y ]. x  e.  y  \/  [. A  /  y ]. y  e.  x  \/  [. A  /  y ]. x  =  y ) ) ).
7:5,6: e11 28522  |-  (. A  e.  B  ->.  ( [. A  /  y ]. ( x  e.  y  \/  y  e.  x  \/  x  =  y )  <->  ( x  e.  A  \/  A  e.  x  \/  x  =  A ) ) ).
qed:7:  |-  ( A  e.  B  ->  ( [. A  /  y ]. ( x  e.  y  \/  y  e.  x  \/  x  =  y )  <->  ( x  e.  A  \/  A  e.  x  \/  x  =  A ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 [. A  /  y ]. ( x  e.  y  \/  y  e.  x  \/  x  =  y
 ) 
 <->  ( x  e.  A  \/  A  e.  x  \/  x  =  A )
 ) )
 
Theoremhbra2VD 28709* Virtual deduction proof of nfra2 2599. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  ( A. y  e.  B A. x  e.  A ph  ->  A. y A. y  e.  B A. x  e.  A ph )
2::  |-  ( A. x  e.  A A. y  e.  B ph  <->  A. y  e.  B A. x  e.  A ph )
3:1,2,?: e00 28614  |-  ( A. x  e.  A A. y  e.  B ph  ->  A. y A. y  e.  B A. x  e.  A ph )
4:2:  |-  A. y ( A. x  e.  A A. y  e.  B ph  <->  A. y  e.  B A. x  e.  A ph )
5:4,?: e0_ 28618  |-  ( A. y A. x  e.  A A. y  e.  B ph  <->  A. y A. y  e.  B A. x  e.  A ph )
qed:3,5,?: e00 28614  |-  ( A. x  e.  A A. y  e.  B ph  ->  A. y A. x  e.  A A. y  e.  B ph )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x  e.  A  A. y  e.  B  ph  ->  A. y A. x  e.  A  A. y  e.  B  ph )
 
TheoremtratrbVD 28710* Virtual deduction proof of tratrb 28355. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  ( Tr  A  /\  A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ).
2:1,?: e1_ 28461  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  Tr  A ).
3:1,?: e1_ 28461  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ).
4:1,?: e1_ 28461  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  B  e.  A ).
5::  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  ( x  e.  y  /\  y  e.  B ) ).
6:5,?: e2 28465  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  x  e.  y ).
7:5,?: e2 28465  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  y  e.  B ).
8:2,7,4,?: e121 28490  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  y  e.  A ).
9:2,6,8,?: e122 28487  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  x  e.  A ).
10::  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B ) ,  B  e.  x  ->.  B  e.  x ).
11:6,7,10,?: e223 28469  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B ) ,  B  e.  x  ->.  ( x  e.  y  /\  y  e.  B  /\  B  e.  x ) ).
12:11:  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  ( B  e.  x  ->  ( x  e.  y  /\  y  e.  B  /\  B  e.  x ) ) ).
13::  |-  -.  ( x  e.  y  /\  y  e.  B  /\  B  e.  x )
14:12,13,?: e20 28573  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  -.  B  e.  x ).
15::  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B ) ,  x  =  B  ->.  x  =  B ).
16:7,15,?: e23 28601  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B ) ,  x  =  B  ->.  y  e.  x ).
17:6,16,?: e23 28601  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B ) ,  x  =  B  ->.  ( x  e.  y  /\  y  e.  x ) ).
18:17:  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  ( x  =  B  ->  ( x  e.  y  /\  y  e.  x ) ) ).
19::  |-  -.  ( x  e.  y  /\  y  e.  x )
20:18,19,?: e20 28573  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  -.  x  =  B ).
21:3,?: e1_ 28461  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  A. y  e.  A  A. x  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ).
22:21,9,4,?: e121 28490  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  [. x  /  x ]. [. B  /  y ]. ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ).
23:22,?: e2 28465  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  [. B  /  y ]. ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ).
24:4,23,?: e12 28570  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  ( x  e.  B  \/  B  e.  x  \/  x  =  B ) ).
25:14,20,24,?: e222 28470  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) ,  ( x  e.  y  /\  y  e.  B )  ->.  x  e.  B ).
26:25:  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  ( ( x  e.  y  /\  y  e.  B )  ->  x  e.  B ) ).
27::  |-  ( A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  ->  A. y A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
28:27,?: e0_ 28618  |-  ( ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->  A. y ( Tr  A  /\  A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) )
29:28,26:  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  A. y ( ( x  e.  y  /\  y  e.  B )  ->  x  e.  B ) ).
30::  |-  ( A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  ->  A. x A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
31:30,?: e0_ 28618  |-  ( ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->  A. x ( Tr  A  /\  A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) )
32:31,29:  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  A. x  A. y ( ( x  e.  y  /\  y  e.  B )  ->  x  e.  B ) ).
33:32,?: e1_ 28461  |-  (. ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->.  Tr  B ).
qed:33:  |-  ( ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A )  ->  Tr  B )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( Tr  A  /\  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A ) 
 ->  Tr  B )
 
Theorem3ax5VD 28711 Virtual deduction proof of 3ax5 28356. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. A. x ( ph  ->  ( ps  ->  ch ) )  ->.  A. x ( ph  ->  ( ps  ->  ch ) ) ).
2:1,?: e1_ 28461  |-  (. A. x ( ph  ->  ( ps  ->  ch ) )  ->.  ( A. x ph  ->  A. x ( ps  ->  ch ) ) ).
3::  |-  ( A. x ( ps  ->  ch )  ->  ( A. x ps  ->  A. x ch ) )
4:2,3,?: e10 28529  |-  (. A. x ( ph  ->  ( ps  ->  ch ) )  ->.  ( A. x ph  ->  ( A. x ps  ->  A. x ch ) ) ).
qed:4:  |-  ( A. x ( ph  ->  ( ps  ->  ch ) )  ->  ( A. x ph  ->  ( A. x ps  ->  A. x ch ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x ( ph  ->  ( ps  ->  ch )
 )  ->  ( A. x ph  ->  ( A. x ps  ->  A. x ch ) ) )
 
Theoremsyl5impVD 28712 Virtual deduction proof of syl5imp 28330. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. ( ph  ->  ( ps  ->  ch ) )  ->.  ( ph  ->  ( ps  ->  ch ) ) ).
2:1,?: e1_ 28461  |-  (. ( ph  ->  ( ps  ->  ch ) )  ->.  ( ps  ->  ( ph  ->  ch ) ) ).
3::  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( th  ->  ps ) ).
4:3,2,?: e21 28576  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( th  ->  ( ph  ->  ch ) ) ).
5:4,?: e2 28465  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( ph  ->  ( th  ->  ch ) ) ).
6:5:  |-  (. ( ph  ->  ( ps  ->  ch ) )  ->.  ( ( th  ->  ps )  ->  ( ph  ->  ( th  ->  ch ) ) ) ).
qed:6:  |-  ( ( ph  ->  ( ps  ->  ch ) )  ->  ( ( th  ->  ps )  ->  ( ph  ->  ( th  ->  ch ) ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  ->  ( ps 
 ->  ch ) )  ->  ( ( th  ->  ps )  ->  ( ph  ->  ( th  ->  ch )
 ) ) )
 
TheoremidiVD 28713 Virtual deduction proof of idi 2. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1::  |-  ph
qed:1,?: e0_ 28618  |-  ph
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   =>    |-  ph
 
TheoremancomsimpVD 28714 Closed form of ancoms 439. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  ( ( ph  /\  ps )  <->  ( ps  /\  ph ) )
qed:1,?: e0_ 28618  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ( ps  /\  ph )  ->  ch ) )
(Contributed by Alan Sare, 25-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps )  ->  ch )  <->  ( ( ps 
 /\  ph )  ->  ch )
 )
 
Theoremssralv2VD 28715* Quantification restricted to a subclass for two quantifiers. ssralv 3239 for two quantifiers. 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. ssralv2 28350 is ssralv2VD 28715 without virtual deductions and was automatically derived from ssralv2VD 28715.
1::  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A  C_  B  /\  C  C_  D ) ).
2::  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  B A. y  e.  D ph ).
3:1:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  A  C_  B ).
4:3,2:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  A A. y  e.  D ph ).
5:4:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x ( x  e.  A  ->  A. y  e.  D ph ) ).
6:5:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  ( x  e.  A  ->  A. y  e.  D ph ) ).
7::  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  x  e.  A ).
8:7,6:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  A. y  e.  D ph ).
9:1:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  C  C_  D ).
10:9,8:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  A. y  e.  C ph ).
11:10:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  ( x  e.  A  ->  A. y  e.  C ph ) ).
12::  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A. x ( A  C_  B  /\  C  C_  D ) )
13::  |-  ( A. x  e.  B A. y  e.  D ph  ->  A. x A. x  e.  B A. y  e.  D ph )
14:12,13,11:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x ( x  e.  A  ->  A. y  e.  C ph ) ).
15:14:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  A A. y  e.  C ph ).
16:15:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A. x  e.  B A. y  e.  D ph  ->  A. x  e.  A A. y  e.  C ph ) ).
qed:16:  |-  ( ( A  C_  B  /\  C  C_  D )  ->  ( A. x  e.  B A. y  e.  D ph  ->  A. x  e.  A A. y  e.  C ph ) )
(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( A  C_  B  /\  C  C_  D )  ->  ( A. x  e.  B  A. y  e.  D  ph  ->  A. x  e.  A  A. y  e.  C  ph ) )
 
TheoremordelordALTVD 28716 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4416 using the Axiom of Regularity indirectly through dford2 7323. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that  _E  Fr  A because this is inferred by the Axiom of Regularity. 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. ordelordALT 28357 is ordelordALTVD 28716 without virtual deductions and was automatically derived from ordelordALTVD 28716 using the tools program translate..without..overwriting.cmd and Metamath's minimize command.
1::  |-  (. ( Ord  A  /\  B  e.  A )  ->.  ( Ord  A  /\  B  e.  A ) ).
2:1:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Ord  A ).
3:1:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  B  e.  A ).
4:2:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Tr  A ).
5:2:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ).
6:4,3:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  B  C_  A ).
7:6,6,5:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  B  A. y  e.  B ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ).
8::  |-  ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
9:8:  |-  A. y ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
10:9:  |-  A. y  e.  A ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
11:10:  |-  ( A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
12:11:  |-  A. x ( A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
13:12:  |-  A. x  e.  A ( A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
14:13:  |-  ( A. x  e.  A A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. x  e.  A A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
15:14,5:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ).
16:4,15,3:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Tr  B ).
17:16,7:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Ord  B ).
qed:17:  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )
(Contributed by Alan Sare, 12-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( Ord  A  /\  B  e.  A )  ->  Ord  B )
 
TheoremequncomVD 28717 If a class equals the union of two other classes, then it equals the union of those two classes commuted. 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. equncom 3322 is equncomVD 28717 without virtual deductions and was automatically derived from equncomVD 28717.
1::  |-  (. A  =  ( B  u.  C )  ->.  A  =  ( B  u.  C ) ).
2::  |-  ( B  u.  C )  =  ( C  u.  B )
3:1,2:  |-  (. A  =  ( B  u.  C )  ->.  A  =  ( C  u.  B ) ).
4:3:  |-  ( A  =  ( B  u.  C )  ->  A  =  ( C  u.  B ) )
5::  |-  (. A  =  ( C  u.  B )  ->.  A  =  ( C  u.  B ) ).
6:5,2:  |-  (. A  =  ( C  u.  B )  ->.  A  =  ( B  u.  C ) ).
7:6:  |-  ( A  =  ( C  u.  B )  ->  A  =  ( B  u.  C ) )
8:4,7:  |-  ( A  =  ( B  u.  C )  <->  A  =  ( C  u.  B ) )
(Contributed by Alan Sare, 17-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  =  ( B  u.  C )  <->  A  =  ( C  u.  B ) )
 
TheoremequncomiVD 28718 Inference form of equncom 3322. 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. equncomi 3323 is equncomiVD 28718 without virtual deductions and was automatically derived from equncomiVD 28718.
h1::  |-  A  =  ( B  u.  C )
qed:1:  |-  A  =  ( C  u.  B )
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  =  ( B  u.  C )   =>    |-  A  =  ( C  u.  B )
 
TheoremsucidALTVD 28719 A set belongs to its successor. Alternate proof of sucid 4473. 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. sucidALT 28720 is sucidALTVD 28719 without virtual deductions and was automatically derived from sucidALTVD 28719. This proof illustrates that completeusersproof.cmd will generate a Metamath proof from any User's Proof which is "conventional" in the sense that no step is a virtual deduction, provided that all necessary unification theorems and transformation deductions are in set.mm. completeusersproof.cmd automatically converts such a conventional proof into a Virtual Deduction proof for which each step happens to be a 0-virtual hypothesis virtual deduction. The user does not need to search for reference theorem labels or deduction labels nor does he(she) need to use theorems and deductions which unify with reference theorems and deductions in set.mm. All that is necessary is that each theorem or deduction of the User's Proof unifies with some reference theorem or deduction in set.mm or is a semantic variation of some theorem or deduction which unifies with some reference theorem or deduction in set.mm. The definition of "semantic variation" has not been precisely defined. If it is obvious that a theorem or deduction has the same meaning as another theorem or deduction, then it is a semantic variation of the latter theorem or deduction. For example, step 4 of the User's Proof is a semantic variation of the definition (axiom)  suc  A  =  ( A  u.  { A } ), which unifies with df-suc 4400, a reference definition (axiom) in set.mm. Also, a theorem or deduction is said to be a semantic variation of another theorem or deduction if it is obvious upon cursory inspection that it has the same meaning as a weaker form of the latter theorem or deduction. For example, the deduction  Ord  A infers  A. x  e.  A A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x ) is a semantic variation of the theorem  ( Ord  A  <->  ( Tr  A  /\  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ) ), which unifies with the set.mm reference definition (axiom) dford2 7323.
h1::  |-  A  e.  _V
2:1:  |-  A  e.  { A }
3:2:  |-  A  e.  ( { A }  u.  A )
4::  |-  suc  A  =  ( { A }  u.  A )
qed:3,4:  |-  A  e.  suc  A
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  A  e.  suc  A
 
TheoremsucidALT 28720 A set belongs to its successor. This proof was automatically derived from sucidALTVD 28719 using translatewithout_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  A  e.  suc  A
 
TheoremsucidVD 28721 A set belongs to its successor. 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. sucid 4473 is sucidVD 28721 without virtual deductions and was automatically derived from sucidVD 28721.
h1::  |-  A  e.  _V
2:1:  |-  A  e.  { A }
3:2:  |-  A  e.  ( A  u.  { A } )
4::  |-  suc  A  =  ( A  u.  { A } )
qed:3,4:  |-  A  e.  suc  A
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  A  e.  suc  A
 
Theoremimbi12VD 28722 Implication form of imbi12i 316. 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. imbi12 28338 is imbi12VD 28722 without virtual deductions and was automatically derived from imbi12VD 28722.
1::  |-  (. ( ph  <->  ps )  ->.  ( ph  <->  ps ) ).
2::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ch  <->  th ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ph  ->  ch ) ).
4:1,3:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  ch ) ).
5:2,4:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  th ) ).
6:5:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ph  ->  ch )  ->  ( ps  ->  th ) ) ).
7::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ps  ->  th ) ).
8:1,7:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  th ) ).
9:2,8:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  ch ) ).
10:9:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ps  ->  th )  ->  ( ph  ->  ch ) ) ).
11:6,10:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ).
12:11:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) ).
qed:12:  |-  ( ( ph  <->  ps )  ->  ( ( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  <->  ps )  ->  (
 ( ch  <->  th )  ->  (
 ( ph  ->  ch )  <->  ( ps  ->  th )
 ) ) )
 
Theoremimbi13VD 28723 Join three logical equivalences to form equivalence of implications. 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. imbi13 28339 is imbi13VD 28723 without virtual deductions and was automatically derived from imbi13VD 28723.
1::  |-  (. ( ph  <->  ps )  ->.  ( ph  <->  ps ) ).
2::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ch  <->  th ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ta  <->  et ) ).
4:2,3:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ( ch  ->  ta )  <->  ( th  ->  et ) ) ).
5:1,4:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ).
6:5:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ).
7:6:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ) ).
qed:7:  |-  ( ( ph  <->  ps )  ->  ( ( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  <->  ps )  ->  (
 ( ch  <->  th )  ->  (
 ( ta  <->  et )  ->  (
 ( ph  ->  ( ch 
 ->  ta ) )  <->  ( ps  ->  ( th  ->  et )
 ) ) ) ) )
 
Theoremsbcim2gVD 28724 Distribution of class substitution over a left-nested implication. Similar to sbcimg 3034. 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. sbcim2g 28358 is sbcim2gVD 28724 without virtual deductions and was automatically derived from sbcim2gVD 28724.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2::  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ).
3:1,2:  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ).
4:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ps  ->  ch )  <->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
5:3,4:  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
6:5:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) ).
7::  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
8:4,7:  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ).
9:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ) ).
10:8,9:  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ).
11:10:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ) ).
12:6,11:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) ).
qed:12:  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  (
 [. A  /  x ].
 ps  ->  [. A  /  x ].
 ch ) ) ) )
 
TheoremsbcbiVD 28725 Implication form of sbcbiiOLD 3049. 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. sbcbi 28359 is sbcbiVD 28725 without virtual deductions and was automatically derived from sbcbiVD 28725.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2::  |-  (. A  e.  B ,. A. x ( ph  <->  ps )  ->.  A. x ( ph  <->  ps ) ).
3:1,2:  |-  (. A  e.  B ,. A. x ( ph  <->  ps )  ->.  [. A  /  x ]. ( ph  <->  ps ) ).
4:1,3:  |-  (. A  e.  B ,. A. x ( ph  <->  ps )  ->.  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ).
5:4:  |-  (. A  e.  B  ->.  ( A. x ( ph  <->  ps )  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ) ).
qed:5:  |-  ( A  e.  B  ->  ( A. x ( ph  <->  ps )  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 A. x ( ph  <->  ps )  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ].
 ps ) ) )
 
TheoremtrsbcVD 28726* Formula-building inference rule for class substitution, substituting a class variable for the set variable of the transitivity predicate. 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. trsbc 28360 is trsbcVD 28726 without virtual deductions and was automatically derived from trsbcVD 28726.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
3:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) ).
4:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) ).
5:1,2,3,4:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ).
6:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) ) ) ).
7:5,6:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ).
8::  |-  ( ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
9:7,8:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
10::  |-  ( ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
11:10:  |-  A. x ( ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
12:1,11:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
13:9,12:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
14:13:  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
15:14:  |-  (. A  e.  B  ->.  ( A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
16:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
17:15,16:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
18:17:  |-  (. A  e.  B  ->.  A. z ( [. A  /  x ]. A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
19:18:  |-  (. A  e.  B  ->.  ( A. z [. A  /  x ]. A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
20:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
21:19,20:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
22::  |-  ( Tr  A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
23:21,22:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A ) ).
24::  |-  ( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
25:24:  |-  A. x ( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
26:1,25:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
27:23,26:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  Tr  A ) ).
qed:27:  |-  ( A  e.  B  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 [. A  /  x ].
 Tr  x  <->  Tr  A ) )
 
TheoremtruniALTVD 28727* The union of a class of transitive sets is transitive. 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. truniALT 28361 is truniALTVD 28727 without virtual deductions and was automatically derived from truniALTVD 28727.
1::  |-  (. A. x  e.  A Tr  x  ->.  A. x  e.  A  Tr  x ).
2::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  ( z  e.  y  /\  y  e.  U. A ) ).
3:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  z  e.  y ).
4:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  y  e.  U. A ).
5:4:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  E. q ( y  e.  q  /\  q  e.  A ) ).
6::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  ( y  e.  q  /\  q  e.  A ) ).
7:6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  y  e.  q ).
8:6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  q  e.  A ).
9:1,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  [ q  /  x ] Tr  x ).
10:8,9:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  Tr  q ).
11:3,7,10:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  z  e.  q ).
12:11,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  z  e.  U. A ).
13:12:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ).
14:13:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  A. q ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ).
15:14:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  ( E. q ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ).
16:5,15:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  z  e.  U. A ).
17:16:  |-  (. A. x  e.  A Tr  x  ->.  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A ) ).
18:17:  |-  (. A. x  e.  A Tr  x  ->.  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A ) ).
19:18:  |-  (. A. x  e.  A Tr  x  ->.  Tr  U. A ).
qed:19:  |-  ( A. x  e.  A Tr  x  ->  Tr  U. A )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
 
Theoremee33VD 28728 Non-virtual deduction form of e33 28580. 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. ee33 28340 is ee33VD 28728 without virtual deductions and was automatically derived from ee33VD 28728.
h1::  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
h2::  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
h3::  |-  ( th  ->  ( ta  ->  et ) )
4:1,3:  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  ->  et ) ) ) )
5:4:  |-  ( ta  ->  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) ) )
6:2,5:  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) ) ) ) )
7:6:  |-  ( ps  ->  ( ch  ->  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) ) ) )
8:7:  |-  ( ch  ->  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) ) )
qed:8:  |-  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( ph  ->  ( ps  ->  ( ch  ->  th )
 ) )   &    |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )   &    |-  ( th  ->  ( ta  ->  et ) )   =>    |-  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) )
 
TheoremtrintALTVD 28729* The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 28730. 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. trintALT 28730 is trintALTVD 28729 without virtual deductions and was automatically derived from trintALTVD 28729.
1::  |-  (. A. x  e.  A Tr  x  ->.  A. x  e.  A Tr  x ).
2::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( z  e.  y  /\  y  e.  |^| A ) ).
3:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  z  e.  y ).
4:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  y  e.  |^| A ).
5:4:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q  e.  A y  e.  q ).
6:5:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( q  e.  A  ->  y  e.  q ) ).
7::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  q  e.  A ).
8:7,6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  y  e.  q ).
9:7,1:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  [ q  /  x ] Tr  x ).
10:7,9:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  Tr  q ).
11:10,3,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  z  e.  q ).
12:11:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( q  e.  A  ->  z  e.  q ) ).
13:12:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q ( q  e.  A  ->  z  e.  q ) ).
14:13:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q  e.  A z  e.  q ).
15:3,14:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  z  e.  |^| A ).
16:15:  |-  (. A. x  e.  A Tr  x  ->.  ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  |^| A ) ).
17:16:  |-  (. A. x  e.  A Tr  x  ->.  A. z A. y ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  |^| A ) ).
18:17:  |-  (. A. x  e.  A Tr  x  ->.  Tr  |^| A ).
qed:18:  |-  ( A. x  e.  A Tr  x  ->  Tr  |^| A )
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
 
TheoremtrintALT 28730* The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 28730 is an alternative proof of trint 4130. trintALT 28730 is trintALTVD 28729 without virtual deductions and was automatically derived from trintALTVD 28729 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 28731 The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3431. 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. undif3 3431 is undif3VD 28731 without virtual deductions and was automatically derived from undif3VD 28731.
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 ) )
 
TheoremsbcssVD 28732 Virtual deduction proof of sbcss 3566. 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. sbcss 3566 is sbcssVD 28732 without virtual deductions and was automatically derived from sbcssVD 28732.
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 28733 Virtual deduction proof of csbing 3378. 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. csbing 3378 is csbingVD 28733 without virtual deductions and was automatically derived from csbingVD 28733.
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 28734* Virtual deduction proof of onfrALTlem5 28363. 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. onfrALTlem5 28363 is onfrALTlem5VD 28734 without virtual deductions and was automatically derived from onfrALTlem5VD 28734.
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 28735* Virtual deduction proof of onfrALTlem4 28364. 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. onfrALTlem4 28364 is onfrALTlem4VD 28735 without virtual deductions and was automatically derived from onfrALTlem4VD 28735.
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 28736* Virtual deduction proof of onfrALTlem3 28365. 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. onfrALTlem3 28365 is onfrALTlem3VD 28736 without virtual deductions and was automatically derived from onfrALTlem3VD 28736.
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 )  =  (/) ).
 
Theoremsimplbi2comgVD 28737 Virtual deduction proof of simplbi2comg 1363. 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. simplbi2comg 1363 is simplbi2comgVD 28737 without virtual deductions and was automatically derived from simplbi2comgVD 28737.
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 28738* Virtual deduction proof of onfrALTlem2 28367. 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. onfrALTlem2 28367 is onfrALTlem2VD 28738 without virtual deductions and was automatically derived from onfrALTlem2VD 28738.
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 )