HomeHome Metamath Proof Explorer
Theorem List (p. 336 of 379)
< 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-25813)
  Hilbert Space Explorer  Hilbert Space Explorer
(25814-27338)
  Users' Mathboxes  Users' Mathboxes
(27339-37825)
 

Theorem List for Metamath Proof Explorer - 33501-33600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremunipwr 33501 A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 4687. The proof of this theorem was automatically generated from unipwrVD 33500 using a tools command file , translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  C_ 
 U. ~P A
 
TheoremsstrALT2VD 33502 Virtual deduction proof of sstrALT2 33503. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
 
TheoremsstrALT2 33503 Virtual deduction proof of sstr 3497, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 33502 using the command file translatewithout_overwriting.cmd . It was not minimized because the automated minimization excluding duplicates generates a minimized proof which, although not directly containing any duplicates, indirectly contains a duplicate. That is, the trace back of the minimized proof contains a duplicate. This is undesirable because some step(s) of the minimized proof use the proven theorem. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
 
TheoremsuctrALT2VD 33504 Virtual deduction proof of suctrALT2 33505. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  Tr  suc  A )
 
TheoremsuctrALT2 33505 Virtual deduction proof of suctr 4951. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 33504 using the tools command file translatewithout_overwritingminimize_excludingduplicates.cmd . (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  Tr  suc  A )
 
Theoremelex2VD 33506* Virtual deduction proof of elex2 3107. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  E. x  x  e.  B )
 
Theoremelex22VD 33507* Virtual deduction proof of elex22 3108. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( A  e.  B  /\  A  e.  C ) 
 ->  E. x ( x  e.  B  /\  x  e.  C ) )
 
Theoremeqsbc3rVD 33508* Virtual deduction proof of eqsbc3r 3375. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 [. A  /  x ]. C  =  x  <->  C  =  A ) )
 
Theoremzfregs2VD 33509* Virtual deduction proof of zfregs2 8167. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  =/=  (/)  ->  -.  A. x  e.  A  E. y ( y  e.  A  /\  y  e.  x )
 )
 
Theoremtpid3gVD 33510 Virtual deduction proof of tpid3g 4130. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  A  e.  { C ,  D ,  A }
 )
 
Theoremen3lplem1VD 33511* Virtual deduction proof of en3lplem1 8034. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( A  e.  B  /\  B  e.  C  /\  C  e.  A )  ->  ( x  =  A  ->  E. y ( y  e.  { A ,  B ,  C }  /\  y  e.  x ) ) )
 
Theoremen3lplem2VD 33512* Virtual deduction proof of en3lplem2 8035. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( A  e.  B  /\  B  e.  C  /\  C  e.  A )  ->  ( x  e.  { A ,  B ,  C }  ->  E. y
 ( y  e.  { A ,  B ,  C }  /\  y  e.  x ) ) )
 
Theoremen3lpVD 33513 Virtual deduction proof of en3lp 8036. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  -.  ( A  e.  B  /\  B  e.  C  /\  C  e.  A )
 
21.27.8  Theorems proved using Virtual Deduction with mmj2 assistance
 
Theoremsimplbi2VD 33514 Virtual deduction proof of simplbi2 625. 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 ) )
3:1,?: e0a 33437  |-  ( ( ps  /\  ch )  ->  ph )
qed:3,?: e0a 33437  |-  ( ps  ->  ( ch  ->  ph ) )
The proof of simplbi2 625 was automatically derived from it. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( ps  /\  ch ) )   =>    |-  ( ps  ->  ( ch  ->  ph ) )
 
Theorem3ornot23VD 33515 Virtual deduction proof of 3ornot23 33146. 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 )  ->.  ( -.  ph  /\  -.  ps ) ).
2::  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ( ch  \/  ph  \/  ps ) ).
3:1,?: e1a 33281  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ph ).
4:1,?: e1a 33281  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ps ).
5:3,4,?: e11 33342  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ( ph  \/  ps ) ).
6:2,?: e2 33285  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ( ch  \/  ( ph  \/  ps ) ) ).
7:5,6,?: e12 33389  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ch ).
8:7:  |-  (. ( -.  ph  /\  -.  ps )  ->.  ( ( ch  \/  ph  \/  ps )  ->  ch ) ).
qed:8:  |-  ( ( -.  ph  /\  -.  ps )  ->  ( ( ch  \/  ph  \/  ps )  ->  ch ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( -.  ph  /\  -.  ps )  ->  ( ( ch  \/  ph  \/  ps )  ->  ch ) )
 
Theoremorbi1rVD 33516 Virtual deduction proof of orbi1r 33147. 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 )  ->.  ( ph  <->  ps ) ).
2::  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ph ) ).
3:2,?: e2 33285  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ph  \/  ch ) ).
4:1,3,?: e12 33389  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ps  \/  ch ) ).
5:4,?: e2 33285  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ps ) ).
6:5:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) ) ).
7::  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ps ) ).
8:7,?: e2 33285  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ps  \/  ch ) ).
9:1,8,?: e12 33389  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ph  \/  ch ) ).
10:9,?: e2 33285  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ph ) ).
11:10:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) ) ).
12:6,11,?: e11 33342  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ph )  <->  ( ch  \/  ps ) ) ).
qed:12:  |-  ( ( ph  <->  ps )  ->  ( ( ch  \/  ph )  <->  ( ch  \/  ps ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  <->  ps )  ->  (
 ( ch  \/  ph ) 
 <->  ( ch  \/  ps ) ) )
 
Theorembitr3VD 33517 Virtual deduction proof of bitr3 33148. 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 )  ->.  ( ph  <->  ps ) ).
2:1,?: e1a 33281  |-  (. ( ph  <->  ps )  ->.  ( ps  <->  ph ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ph  <->  ch )  ->.  ( ph  <->  ch ) ).
4:3,?: e2 33285  |-  (. ( ph  <->  ps ) ,. ( ph  <->  ch )  ->.  ( ch  <->  ph ) ).
5:2,4,?: e12 33389  |-  (. ( ph  <->  ps ) ,. ( ph  <->  ch )  ->.  ( ps  <->  ch ) ).
6:5:  |-  (. ( ph  <->  ps )  ->.  ( ( ph  <->  ch )  ->  ( ps  <->  ch ) ) ).
qed:6:  |-  ( ( ph  <->  ps )  ->  ( ( ph  <->  ch )  ->  ( ps  <->  ch ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  <->  ps )  ->  (
 ( ph  <->  ch )  ->  ( ps 
 <->  ch ) ) )
 
Theorem3orbi123VD 33518 Virtual deduction proof of 3orbi123 33149. 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  <->  et ) )  ->.  ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) ) ).
2:1,?: e1a 33281  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ph  <->  ps ) ).
3:1,?: e1a 33281  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ch  <->  th ) ).
4:1,?: e1a 33281  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ta  <->  et ) ).
5:2,3,?: e11 33342  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ph  \/  ch )  <->  ( ps  \/  th ) ) ).
6:5,4,?: e11 33342  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ( ph  \/  ch )  \/  ta )  <->  ( ( ps  \/  th )  \/  et ) ) ).
7:?:  |-  ( ( ( ph  \/  ch )  \/  ta )  <->  ( ph  \/  ch  \/  ta ) )
8:6,7,?: e10 33348  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ph  \/  ch  \/  ta )  <->  ( ( ps  \/  th )  \/  et ) ) ).
9:?:  |-  ( ( ( ps  \/  th )  \/  et )  <->  ( ps  \/  th  \/  et ) )
10:8,9,?: e10 33348  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ph  \/  ch  \/  ta )  <->  ( ps  \/  th  \/  et ) ) ).
qed:10:  |-  ( ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->  ( ( ph  \/  ch  \/  ta )  <->  ( ps  \/  th  \/  et ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  <->  ps )  /\  ( ch 
 <-> 
 th )  /\  ( ta 
 <->  et ) )  ->  ( ( ph  \/  ch 
 \/  ta )  <->  ( ps  \/  th 
 \/  et ) ) )
 
Theoremsbc3orgVD 33519 Virtual deduction proof of sbc3orgOLD 33171. 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,?: e1a 33281  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ( ph  \/  ps )  \/  ch )  <->  ( [. A  /  x ]. ( ph  \/  ps )  \/  [. A  /  x ]. ch ) ) ).
3::  |-  ( ( ( ph  \/  ps )  \/  ch )  <->  ( ph  \/  ps  \/  ch ) )
32:3:  |-  A. x ( ( ( ph  \/  ps )  \/  ch )  <->  ( ph  \/  ps  \/  ch ) )
33:1,32,?: e10 33348  |-  (. A  e.  B  ->.  [. A  /  x ]. ( ( ( ph  \/  ps )  \/  ch )  <->  ( ph  \/  ps  \/  ch ) ) ).
4:1,33,?: e11 33342  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ( ph  \/  ps )  \/  ch )  <->  [. A  /  x ]. ( ph  \/  ps  \/  ch ) ) ).
5:2,4,?: e11 33342  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  \/  ps  \/  ch )  <->  ( [. A  /  x ]. ( ph  \/  ps )  \/  [. A  /  x ]. ch ) ) ).
6:1,?: e1a 33281  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  \/  ps )  <->  ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps ) ) ).
7:6,?: e1a 33281  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. ( ph  \/  ps )  \/  [. A  /  x ]. ch )  <->  ( ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps )  \/  [. A  /  x ]. ch ) ) ).
8:5,7,?: e11 33342  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  \/  ps  \/  ch )  <->  ( ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps )  \/  [. A  /  x ]. ch ) ) ).
9:?:  |-  ( ( ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps )  \/  [. A  /  x ]. ch )  <->  ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps  \/  [. A  /  x ]. ch ) )
10:8,9,?: e10 33348  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  \/  ps  \/  ch )  <->  ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps  \/  [. A  /  x ]. ch ) ) ).
qed:10:  |-  ( A  e.  B  ->  ( [. 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  e.  B  ->  (
 [. A  /  x ]. ( ph  \/  ps  \/  ch )  <->  ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps  \/  [. A  /  x ].
 ch ) ) )
 
Theorem19.21a3con13vVD 33520* Virtual deduction proof of alrim3con13v 33172. 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 33285  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ps ).
4:2,?: e2 33285  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ph ).
5:2,?: e2 33285  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ch ).
6:1,4,?: e12 33389  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ph ).
7:3,?: e2 33285  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ps ).
8:5,?: e2 33285  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ch ).
9:7,6,8,?: e222 33290  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ( A. x ps  /\  A. x ph  /\  A. x ch ) ).
10:9,?: e2 33285  |-  (. ( 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 33521 Virtual deduction proof of exbir 33087. 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 33389  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( ch  <->  th ) ).
6:3,5,?: e32 33423  |-  (. ( ( 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,?: e1a 33281  |-  (. ( ( 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 33522 Virtual deduction proof of exbiri 622. 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 33348  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 33395  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 33423  |-  (. 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 33523* Virtual deduction proof of rspsbc2 33173. 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 33413  |-  (. 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 33413  |-  (. 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 33420  |-  (. 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 33524 Virtual deduction proof of 3impexp 33088. 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 33348  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ( ph  /\  ps )  /\  ch )  ->  th ) ).
4:3,?: e1a 33281  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ph  /\  ps )  ->  ( ch  ->  th ) ) ).
5:4,?: e1a 33281  |-  (. ( ( 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,?: e1a 33281  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ph  /\  ps )  ->  ( ch  ->  th ) ) ).
9:8,?: e1a 33281  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ( ph  /\  ps )  /\  ch )  ->  th ) ).
10:2,9,?: e01 33345  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  th ) ).
11:10:  |-  ( ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->  ( ( ph  /\  ps  /\  ch )  ->  th ) )
qed:6,11,?: e00 33433  |-  ( ( ( 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 33525 Virtual deduction proof of 3impexpbicom 33089. 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 33348  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
4:3,?: e1a 33281  |-  (. ( ( 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,?: e1a 33281  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
8:7,2,?: e10 33348  |-  (. ( 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 33433  |-  ( ( ( 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 33526 Virtual deduction proof of 3impexpbicomi 33090. 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,?: e0a 33437  |-  ( 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 33527* Virtual deduction proof of sbcoreleleq 33174. 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,?: e1a 33281  |-  (. A  e.  B  ->.  ( [. A  /  y ]. x  e.  y  <->  x  e.  A ) ).
3:1,?: e1a 33281  |-  (. A  e.  B  ->.  ( [. A  /  y ]. y  e.  x  <->  A  e.  x ) ).
4:1,?: e1a 33281  |-  (. A  e.  B  ->.  ( [. A  /  y ]. x  =  y  <->  x  =  A ) ).
5:2,3,4,?: e111 33328  |-  (. 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,?: e1a 33281  |-  (. 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 33342  |-  (. 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 33528* Virtual deduction proof of nfra2 2830. 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 33433  |-  ( 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,?: e0a 33437  |-  ( 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 33433  |-  ( 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 33529* Virtual deduction proof of tratrb 33175. 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,?: e1a 33281  |-  (. ( 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,?: e1a 33281  |-  (. ( 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,?: e1a 33281  |-  (. ( 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 33285  |-  (. ( 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 33285  |-  (. ( 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 33310  |-  (. ( 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 33307  |-  (. ( 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 33289  |-  (. ( 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 33392  |-  (. ( 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 33420  |-  (. ( 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 33420  |-  (. ( 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 33392  |-  (. ( 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,?: e1a 33281  |-  (. ( 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 33310  |-  (. ( 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 33285  |-  (. ( 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 33389  |-  (. ( 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 33290  |-  (. ( 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,?: e0a 33437  |-  ( ( 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,?: e0a 33437  |-  ( ( 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,?: e1a 33281  |-  (. ( 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 )
 
Theoremal2imVD 33530 Virtual deduction proof of al2im 1622. 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,?: e1a 33281  |-  (. 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 33348  |-  (. 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 33531 Virtual deduction proof of syl5imp 33150. 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,?: e1a 33281  |-  (. ( ph  ->  ( ps  ->  ch ) )  ->.  ( ps  ->  ( ph  ->  ch ) ) ).
3::  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( th  ->  ps ) ).
4:3,2,?: e21 33395  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( th  ->  ( ph  ->  ch ) ) ).
5:4,?: e2 33285  |-  (. ( 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 33532 Virtual deduction proof of idiALT 33086. 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,?: e0a 33437  |-  ph
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   =>    |-  ph
 
TheoremancomstVD 33533 Closed form of ancoms 453. 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,?: e0a 33437  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ( ps  /\  ph )  ->  ch ) )
The proof of ancomst 452 is derived automatically from it. (Contributed by Alan Sare, 25-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ph  /\  ps )  ->  ch )  <->  ( ( ps 
 /\  ph )  ->  ch )
 )
 
Theoremssralv2VD 33534* Quantification restricted to a subclass for two quantifiers. ssralv 3549 for two quantifiers. 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. ssralv2 33169 is ssralv2VD 33534 without virtual deductions and was automatically derived from ssralv2VD 33534.
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 33535 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4890 using the Axiom of Regularity indirectly through dford2 8040. 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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ordelordALT 33176 is ordelordALTVD 33535 without virtual deductions and was automatically derived from ordelordALTVD 33535 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 33536 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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. equncom 3634 is equncomVD 33536 without virtual deductions and was automatically derived from equncomVD 33536.
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 33537 Inference form of equncom 3634. 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. equncomi 3635 is equncomiVD 33537 without virtual deductions and was automatically derived from equncomiVD 33537.
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 33538 A set belongs to its successor. Alternate proof of sucid 4947. 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. sucidALT 33539 is sucidALTVD 33538 without virtual deductions and was automatically derived from sucidALTVD 33538. 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 4874, 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 8040.
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 33539 A set belongs to its successor. This proof was automatically derived from sucidALTVD 33538 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 33540 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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sucid 4947 is sucidVD 33540 without virtual deductions and was automatically derived from sucidVD 33540.
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 33541 Implication form of imbi12i 326. 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. imbi12 322 is imbi12VD 33541 without virtual deductions and was automatically derived from imbi12VD 33541.
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 33542 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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi13 33158 is imbi13VD 33542 without virtual deductions and was automatically derived from imbi13VD 33542.
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 33543 Distribution of class substitution over a left-nested implication. Similar to sbcimg 3355. 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. sbcim2g 33177 is sbcim2gVD 33543 without virtual deductions and was automatically derived from sbcim2gVD 33543.
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 33544 Implication form of sbcbiiOLD 3374. 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. sbcbi 33178 is sbcbiVD 33544 without virtual deductions and was automatically derived from sbcbiVD 33544.
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 33545* Formula-building inference rule for class substitution, substituting a class variable for the setvar 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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc 33179 is trsbcVD 33545 without virtual deductions and was automatically derived from trsbcVD 33545.
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 33546* 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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. truniALT 33180 is truniALTVD 33546 without virtual deductions and was automatically derived from truniALTVD 33546.
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 33547 Non-virtual deduction form of e33 33399. 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. ee33 33159 is ee33VD 33547 without virtual deductions and was automatically derived from ee33VD 33547.
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 33548* The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 33549. 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. trintALT 33549 is trintALTVD 33548 without virtual deductions and was automatically derived from trintALTVD 33548.
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 33549* The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 33549 is an alternative proof of trint 4545. trintALT 33549 is trintALTVD 33548 without virtual deductions and was automatically derived from trintALTVD 33548 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 33550 The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3744. 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 3744 is undif3VD 33550 without virtual deductions and was automatically derived from undif3VD 33550.
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 33551 Virtual deduction proof of sbcssg 3925. 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 3925 is sbcssgVD 33551 without virtual deductions and was automatically derived from sbcssgVD 33551.
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 33552 Virtual deduction proof of csbingOLD 3847. 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 3847 is csbingVD 33552 without virtual deductions and was automatically derived from csbingVD 33552.
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 33553* Virtual deduction proof of onfrALTlem5 33182. 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 33182 is onfrALTlem5VD 33553 without virtual deductions and was automatically derived from onfrALTlem5VD 33553.
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 33554* Virtual deduction proof of onfrALTlem4 33183. 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 33183 is onfrALTlem4VD 33554 without virtual deductions and was automatically derived from onfrALTlem4VD 33554.
1::  |-  y  e.  _V
2:1:  |-  ( [. y  /  x ]. ( a  i^i  x )  =  (/)  <->  [_  y