HomeHome Metamath Proof Explorer
Theorem List (p. 274 of 309)
< 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-21328)
  Hilbert Space Explorer  Hilbert Space Explorer
(21329-22851)
  Users' Mathboxes  Users' Mathboxes
(22852-30843)
 

Theorem List for Metamath Proof Explorer - 27301-27400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
TheoremsstrALT2 27301 Virtual deduction proof of sstr 3108, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 27300 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 27302 Virtual deduction proof of suctrALT2 27303. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  Tr  suc  A )
 
TheoremsuctrALT2 27303 Virtual deduction proof of suctr 4368. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 27302 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 27304* Virtual deduction proof of elex2 2739. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  E. x  x  e.  B )
 
Theoremelex22VD 27305* Virtual deduction proof of elex22 2738. (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 27306* Virtual deduction proof of eqsbc3r 2978. (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 27307* Virtual deduction proof of zfregs2 7299. (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 27308 Virtual deduction proof of tpid3g 3645. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  A  e.  { C ,  D ,  A }
 )
 
Theoremen3lplem1VD 27309* Virtual deduction proof of en3lplem1 7300. (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 27310* Virtual deduction proof of en3lplem2 7301. (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 27311 Virtual deduction proof of en3lp 7302. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  -.  ( A  e.  B  /\  B  e.  C  /\  C  e.  A )
 
16.20.5  Theorems proved using virtual deduction with mmj2 assistance
 
Theoremsimplbi2VD 27312 Virtual deduction proof of simplbi2 611. 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,?: e0_ 27237  |-  ( ( ps  /\  ch )  ->  ph )
qed:3,?: e0_ 27237  |-  ( ps  ->  ( ch  ->  ph ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( ph 
 <->  ( ps  /\  ch ) )   =>    |-  ( ps  ->  ( ch  ->  ph ) )
 
Theorem3ornot23VD 27313 Virtual deduction proof of 3ornot23 26963. 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,?: e1_ 27089  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ph ).
4:1,?: e1_ 27089  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ps ).
5:3,4,?: e11 27150  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ( ph  \/  ps ) ).
6:2,?: e2 27093  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ( ch  \/  ( ph  \/  ps ) ) ).
7:5,6,?: e12 27189  |-  (. ( -.  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 27314 Virtual deduction proof of orbi1r 26964. 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 27093  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ph  \/  ch ) ).
4:1,3,?: e12 27189  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ps  \/  ch ) ).
5:4,?: e2 27093  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ps ) ).
6:5:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) ) ).
7::  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ps ) ).
8:7,?: e2 27093  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ps  \/  ch ) ).
9:1,8,?: e12 27189  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ph  \/  ch ) ).
10:9,?: e2 27093  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ph ) ).
11:10:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) ) ).
12:6,11,?: e11 27150  |-  (. ( 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 27315 Virtual deduction proof of bitr3 26965. 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,?: e1_ 27089  |-  (. ( ph  <->  ps )  ->.  ( ps  <->  ph ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ph  <->  ch )  ->.  ( ph  <->  ch ) ).
4:3,?: e2 27093  |-  (. ( ph  <->  ps ) ,. ( ph  <->  ch )  ->.  ( ch  <->  ph ) ).
5:2,4,?: e12 27189  |-  (. ( 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 27316 Virtual deduction proof of 3orbi123 26966. 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,?: e1_ 27089  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ph  <->  ps ) ).
3:1,?: e1_ 27089  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ch  <->  th ) ).
4:1,?: e1_ 27089  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ta  <->  et ) ).
5:2,3,?: e11 27150  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ph  \/  ch )  <->  ( ps  \/  th ) ) ).
6:5,4,?: e11 27150  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ( ph  \/  ch )  \/  ta )  <->  ( ( ps  \/  th )  \/  et ) ) ).
7:?:  |-  ( ( ( ph  \/  ch )  \/  ta )  <->  ( ph  \/  ch  \/  ta ) )
8:6,7,?: e10 27157  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ph  \/  ch  \/  ta )  <->  ( ( ps  \/  th )  \/  et ) ) ).
9:?:  |-  ( ( ( ps  \/  th )  \/  et )  <->  ( ps  \/  th  \/  et ) )
10:8,9,?: e10 27157  |-  (. ( ( 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 27317 Virtual deduction proof of sbc3org 26988. 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_ 27089  |-  (. 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 27157  |-  (. A  e.  B  ->.  [. A  /  x ]. ( ( ( ph  \/  ps )  \/  ch )  <->  ( ph  \/  ps  \/  ch ) ) ).
4:1,33,?: e11 27150  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ( ph  \/  ps )  \/  ch )  <->  [. A  /  x ]. ( ph  \/  ps  \/  ch ) ) ).
5:2,4,?: e11 27150  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  \/  ps  \/  ch )  <->  ( [. A  /  x ]. ( ph  \/  ps )  \/  [. A  /  x ]. ch ) ) ).
6:1,?: e1_ 27089  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  \/  ps )  <->  ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps ) ) ).
7:6,?: e1_ 27089  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. ( ph  \/  ps )  \/  [. A  /  x ]. ch )  <->  ( ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps )  \/  [. A  /  x ]. ch ) ) ).
8:5,7,?: e11 27150  |-  (. 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 27157  |-  (. 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 27318* Virtual deduction proof of alrim3con13v 26989. 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 27093  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ps ).
4:2,?: e2 27093  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ph ).
5:2,?: e2 27093  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ch ).
6:1,4,?: e12 27189  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ph ).
7:3,?: e2 27093  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ps ).
8:5,?: e2 27093  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ch ).
9:7,6,8,?: e222 27098  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ( A. x ps  /\  A. x ph  /\  A. x ch ) ).
10:9,?: e2 27093  |-  (. ( 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 27319 Virtual deduction proof of exbir 1361. 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 27189  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( ch  <->  th ) ).
6:3,5,?: e32 27223  |-  (. ( ( 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_ 27089  |-  (. ( ( 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 27320 Virtual deduction proof of exbiri 608. 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 27157  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 27195  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 27223  |-  (. 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 ) ) )
 
Theoremra4sbc2VD 27321* Virtual deduction proof of ra4sbc2 26990. 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 27213  |-  (. 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 27213  |-  (. 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 27220  |-  (. 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 27322 Virtual deduction proof of 3impexp 1362. 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 27157  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ( ph  /\  ps )  /\  ch )  ->  th ) ).
4:3,?: e1_ 27089  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ph  /\  ps )  ->  ( ch  ->  th ) ) ).
5:4,?: e1_ 27089  |-  (. ( ( 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_ 27089  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ph  /\  ps )  ->  ( ch  ->  th ) ) ).
9:8,?: e1_ 27089  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ( ph  /\  ps )  /\  ch )  ->  th ) ).
10:2,9,?: e01 27153  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  th ) ).
11:10:  |-  ( ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->  ( ( ph  /\  ps  /\  ch )  ->  th ) )
qed:6,11,?: e00 27233  |-  ( ( ( 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 27323 Virtual deduction proof of 3impexpbicom 1363. 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 27157  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
4:3,?: e1_ 27089  |-  (. ( ( 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_ 27089  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
8:7,2,?: e10 27157  |-  (. ( 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 27233  |-  ( ( ( 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 27324 Virtual deduction proof of 3impexpbicomi 1364. 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_ 27237  |-  ( 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 27325* Virtual deduction proof of sbcoreleleq 26991. 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_ 27089  |-  (. A  e.  B  ->.  ( [. A  /  y ]. x  e.  y  <->  x  e.  A ) ).
3:1,?: e1_ 27089  |-  (. A  e.  B  ->.  ( [. A  /  y ]. y  e.  x  <->  A  e.  x ) ).
4:1,?: e1_ 27089  |-  (. A  e.  B  ->.  ( [. A  /  y ]. x  =  y  <->  x  =  A ) ).
5:2,3,4,?: e111 27136  |-  (. 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_ 27089  |-  (. 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 27150  |-  (. 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 27326* Virtual deduction proof of nfra2 2559. 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 27233  |-  ( 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_ 27237  |-  ( 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 27233  |-  ( 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 27327* Virtual deduction proof of tratrb 26992. 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_ 27089  |-  (. ( 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_ 27089  |-  (. ( 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_ 27089  |-  (. ( 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 27093  |-  (. ( 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 27093  |-  (. ( 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 27118  |-  (. ( 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 27115  |-  (. ( 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 27097  |-  (. ( 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 27192  |-  (. ( 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 27220  |-  (. ( 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 27220  |-  (. ( 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 27192  |-  (. ( 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_ 27089  |-  (. ( 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 27118  |-  (. ( 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 27093  |-  (. ( 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 27189  |-  (. ( 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 27098  |-  (. ( 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_ 27237  |-  ( ( 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_ 27237  |-  ( ( 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_ 27089  |-  (. ( 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 27328 Virtual deduction proof of 3ax5 26993. 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_ 27089  |-  (. 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 27157  |-  (. 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 27329 Virtual deduction proof of syl5imp 26967. 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_ 27089  |-  (. ( ph  ->  ( ps  ->  ch ) )  ->.  ( ps  ->  ( ph  ->  ch ) ) ).
3::  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( th  ->  ps ) ).
4:3,2,?: e21 27195  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( th  ->  ( ph  ->  ch ) ) ).
5:4,?: e2 27093  |-  (. ( 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 27330 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_ 27237  |-  ph
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   =>    |-  ph
 
TheoremancomsimpVD 27331 Closed form of ancoms 441. 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_ 27237  |-  ( ( ( 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 27332* Quantification restricted to a subclass for two quantifiers. ssralv 3158 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 26987 is ssralv2VD 27332 without virtual deductions and was automatically derived from ssralv2VD 27332.
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 27333 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4307 using the Axiom of Regularity indirectly through dford2 7205. 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 26994 is ordelordALTVD 27333 without virtual deductions and was automatically derived from ordelordALTVD 27333 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 27334 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 3230 is equncomVD 27334 without virtual deductions and was automatically derived from equncomVD 27334.
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 27335 Inference form of equncom 3230. 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 3231 is equncomiVD 27335 without virtual deductions and was automatically derived from equncomiVD 27335.
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 27336 A set belongs to its successor. Alternate proof of sucid 4364. 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 27337 is sucidALTVD 27336 without virtual deductions and was automatically derived from sucidALTVD 27336. 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 4291, a reference definition (axiom) in set.mm. Also, a theorem or deduction is said to be a semantic variation of a 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 7205.
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 27337 A set belongs to its successor. This proof was automatically derived from sucidALTVD 27336 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 27338 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 4364 is sucidVD 27338 without virtual deductions and was automatically derived from sucidVD 27338.
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 27339 Implication form of imbi12i 318. 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 26975 is imbi12VD 27339 without virtual deductions and was automatically derived from imbi12VD 27339.
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 27340 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 26976 is imbi13VD 27340 without virtual deductions and was automatically derived from imbi13VD 27340.
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 27341 Distribution of class substitution over a left-nested implication. Similar to sbcimg 2962. 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 26995 is sbcim2gVD 27341 without virtual deductions and was automatically derived from sbcim2gVD 27341.
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 27342 Implication form of sbcbiiOLD 2977. 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 26996 is sbcbiVD 27342 without virtual deductions and was automatically derived from sbcbiVD 27342.
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 27343* 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 26997 is trsbcVD 27343 without virtual deductions and was automatically derived from trsbcVD 27343.
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 27344* 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 26998 is truniALTVD 27344 without virtual deductions and was automatically derived from truniALTVD 27344.
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 27345 Non-virtual deduction form of e33 27199. 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 26977 is ee33VD 27345 without virtual deductions and was automatically derived from ee33VD 27345.
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 27346* The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 27347. 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 27347 is trintALTVD 27346 without virtual deductions and was automatically derived from trintALTVD 27346.
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 27347* The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 27347 is an alternative proof of trint 4025. trintALT 27347 is trintALTVD 27346 without virtual deductions and was automatically derived from trintALTVD 27346 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 27348 The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3336. 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 3336 is undif3VD 27348 without virtual deductions and was automatically derived from undif3VD 27348.
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 27349 Virtual deduction proof of sbcss 26999. 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 26999 is sbcssVD 27349 without virtual deductions and was automatically derived from sbcssVD 27349.
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 27350 Virtual deduction proof of csbing 3283. 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 3283 is csbingVD 27350 without virtual deductions and was automatically derived from csbingVD 27350.
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 27351* Virtual deduction proof of onfrALTlem5 27000. 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 27000 is onfrALTlem5VD 27351 without virtual deductions and was automatically derived from onfrALTlem5VD 27351.
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