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

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

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

Theorem List for Metamath Proof Explorer - 27701-27800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
TheoremuunTT1 27701 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  T.  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
TheoremuunTT1p1 27702 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
TheoremuunTT1p2 27703 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
TheoremuunT11 27704 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
TheoremuunT11p1 27705 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
TheoremuunT11p2 27706 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ph  /\  T.  )  ->  ps )   =>    |-  ( ph  ->  ps )
 
TheoremuunT12 27707 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ph  /\  ps )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
TheoremuunT12p1 27708 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 (  T.  /\  ps  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
TheoremuunT12p2 27709 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  T.  /\  ps )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
TheoremuunT12p3 27710 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  T.  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
TheoremuunT12p4 27711 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps  /\  T.  )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
TheoremuunT12p5 27712 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  T.  )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
Theoremuun111 27713 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ph  /\  ph )  ->  ps )   =>    |-  ( ph  ->  ps )
 
Theorem3anidm12p1 27714 A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1244 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ps  /\  ph )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
Theorem3anidm12p2 27715 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  ph )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
Theoremuun123 27716 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ch  /\  ps )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
Theoremuun123p1 27717 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ph  /\  ch )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
Theoremuun123p2 27718 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ch  /\  ph  /\  ps )  ->  th )   =>    |-  ( ( ph  /\  ps  /\ 
 ch )  ->  th )
 
Theoremuun123p3 27719 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ps  /\  ch  /\  ph )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
Theoremuun123p4 27720 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ch  /\  ps  /\  ph )  ->  th )   =>    |-  (
 ( ph  /\  ps  /\  ch )  ->  th )
 
Theoremuun2221 27721 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ph  /\  ( ps  /\  ph ) )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
Theoremuun2221p1 27722 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  /\  ( ps 
 /\  ph )  /\  ph )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
Theoremuun2221p2 27723 A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ps  /\  ph )  /\  ph  /\  ph )  ->  ch )   =>    |-  ( ( ps  /\  ph )  ->  ch )
 
Theorem3impdirp1 27724 A deduction unionizing a non-unionized collection of virtual hypotheses. 3impdir 1243 is ~? uun3132 and is in set.mm. 3impdirp1 27724 is ~? uun3132p1. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ( ch  /\  ps )  /\  ( ph  /\ 
 ps ) )  ->  th )   =>    |-  ( ( ph  /\  ch  /\ 
 ps )  ->  th )
 
18.23.4  Theorems proved using virtual deduction
 
TheoremtrsspwALT 27725 Virtual deduction proof of the left-to-right implication of dftr4 4092. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 4092 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  A  C_  ~P A )
 
TheoremtrsspwALT2 27726 Virtual deduction proof of trsspwALT 27725. This proof is the same as the proof of trsspwALT 27725 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A transitive class is a subset of its power class. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  A  C_  ~P A )
 
TheoremtrsspwALT3 27727 Short predicate calculus proof of the left-to-right implication of dftr4 4092. A transitive class is a subset of its power class. This proof was constructed by applying Metamath's minimize command to the proof of trsspwALT2 27726, which is the virtual deduction proof trsspwALT 27725 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  A  C_  ~P A )
 
Theoremsspwtr 27728 Virtual deduction proof of the right-to-left implication of dftr4 4092. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 27728 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  C_  ~P A  ->  Tr  A )
 
TheoremsspwtrALT 27729 Virtual deduction proof of sspwtr 27728. This proof is the same as the proof of sspwtr 27728 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A class which is a subclass of its power class is transitive. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  C_  ~P A  ->  Tr  A )
 
TheoremsspwtrALT2 27730 Short predicate calculus proof of the right-to-left implication of dftr4 4092. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 27729, which is the virtual deduction proof sspwtr 27728 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  C_  ~P A  ->  Tr  A )
 
TheorempwtrVD 27731 Virtual deduction proof of pwtrOLD 27732. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  Tr  ~P A )
 
TheorempwtrOLD 27732 The power class of a transitive class is transitive. The proof of this theorem was automatically generated from pwtrVD 27731 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.) (Moved into main set.mm as pwtr 4198 and may be deleted by mathbox owner, AS. --NM 15-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  Tr  ~P A )
 
TheorempwtrrVD 27733 Virtual deduction proof of pwtrrOLD 27734. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  ( Tr  ~P A  ->  Tr  A )
 
TheorempwtrrOLD 27734 A set is transitive if its power set is. The proof of this theorem was automatically generated from pwtrrVD 27733 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.) (Moved into main set.mm as pwtr 4198 and may be deleted by mathbox owner, AS. --NM 15-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  ( Tr  ~P A  ->  Tr  A )
 
TheoremsnssiALTVD 27735 Virtual deduction proof of snssiALT 27736. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  { A }  C_  B )
 
TheoremsnssiALT 27736 If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 3733. This theorem was automatically generated from snssiALTVD 27735 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  { A }  C_  B )
 
TheoremsnsslVD 27737 Virtual deduction proof of snssl 27738. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  ( { A }  C_  B  ->  A  e.  B )
 
Theoremsnssl 27738 If a singleton is a subclass of another class, then the singleton's element is an element of that other class. This theorem is the right-to-left implication of the biconditional snss 3722. The proof of this theorem was automatically generated from snsslVD 27737 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  e.  _V   =>    |-  ( { A }  C_  B  ->  A  e.  B )
 
TheoremsnelpwrVD 27739 Virtual deduction proof of snelpwi 4192. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  { A }  e.  ~P B )
 
TheoremsnelpwrOLD 27740 If a class is contained in another class, then its singleton is contained in the power class of that other class. This theorem is the left-to-right implication of the biconditional snelpw 4193. Unlike snelpw 4193, 
A may be a proper class. The proof of this theorem was automatically generated from snelpwrVD 27739 using a tools command file, translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Moved to snelpwi 4192 in main set.mm and may be deleted by mathbox owner, AS. --NM 10-Sep-2013.) (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  { A }  e.  ~P B )
 
TheoremunipwrVD 27741 Virtual deduction proof of unipwr 27742. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  C_ 
 U. ~P A
 
Theoremunipwr 27742 A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 4196. The proof of this theorem was automatically generated from unipwrVD 27741 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 27743 Virtual deduction proof of sstrALT2 27744. (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 27744 Virtual deduction proof of sstr 3162, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 27743 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 27745 Virtual deduction proof of suctrALT2 27746. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( Tr  A  ->  Tr  suc  A )
 
TheoremsuctrALT2 27746 Virtual deduction proof of suctr 4447. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 27745 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 27747* Virtual deduction proof of elex2 2775. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  E. x  x  e.  B )
 
Theoremelex22VD 27748* Virtual deduction proof of elex22 2774. (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 27749* Virtual deduction proof of eqsbc3r 3023. (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 27750* Virtual deduction proof of zfregs2 7383. (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 27751 Virtual deduction proof of tpid3g 3715. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  A  e.  { C ,  D ,  A }
 )
 
Theoremen3lplem1VD 27752* Virtual deduction proof of en3lplem1 7384. (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 27753* Virtual deduction proof of en3lplem2 7385. (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 27754 Virtual deduction proof of en3lp 7386. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  -.  ( A  e.  B  /\  B  e.  C  /\  C  e.  A )
 
18.23.5  Theorems proved using virtual deduction with mmj2 assistance
 
Theoremsimplbi2VD 27755 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_ 27680  |-  ( ( ps  /\  ch )  ->  ph )
qed:3,?: e0_ 27680  |-  ( 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 27756 Virtual deduction proof of 3ornot23 27406. 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_ 27532  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ph ).
4:1,?: e1_ 27532  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ps ).
5:3,4,?: e11 27593  |-  (. ( -.  ph  /\  -.  ps )  ->.  -.  ( ph  \/  ps ) ).
6:2,?: e2 27536  |-  (. ( -.  ph  /\  -.  ps ) ,. ( ch  \/  ph  \/  ps )  ->.  ( ch  \/  ( ph  \/  ps ) ) ).
7:5,6,?: e12 27632  |-  (. ( -.  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 27757 Virtual deduction proof of orbi1r 27407. 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 27536  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ph  \/  ch ) ).
4:1,3,?: e12 27632  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ps  \/  ch ) ).
5:4,?: e2 27536  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ph )  ->.  ( ch  \/  ps ) ).
6:5:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) ) ).
7::  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ps ) ).
8:7,?: e2 27536  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ps  \/  ch ) ).
9:1,8,?: e12 27632  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ph  \/  ch ) ).
10:9,?: e2 27536  |-  (. ( ph  <->  ps ) ,. ( ch  \/  ps )  ->.  ( ch  \/  ph ) ).
11:10:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) ) ).
12:6,11,?: e11 27593  |-  (. ( 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 27758 Virtual deduction proof of bitr3 27408. 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_ 27532  |-  (. ( ph  <->  ps )  ->.  ( ps  <->  ph ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ph  <->  ch )  ->.  ( ph  <->  ch ) ).
4:3,?: e2 27536  |-  (. ( ph  <->  ps ) ,. ( ph  <->  ch )  ->.  ( ch  <->  ph ) ).
5:2,4,?: e12 27632  |-  (. ( 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 27759 Virtual deduction proof of 3orbi123 27409. 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_ 27532  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ph  <->  ps ) ).
3:1,?: e1_ 27532  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ch  <->  th ) ).
4:1,?: e1_ 27532  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ta  <->  et ) ).
5:2,3,?: e11 27593  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ph  \/  ch )  <->  ( ps  \/  th ) ) ).
6:5,4,?: e11 27593  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ( ph  \/  ch )  \/  ta )  <->  ( ( ps  \/  th )  \/  et ) ) ).
7:?:  |-  ( ( ( ph  \/  ch )  \/  ta )  <->  ( ph  \/  ch  \/  ta ) )
8:6,7,?: e10 27600  |-  (. ( ( ph  <->  ps )  /\  ( ch  <->  th )  /\  ( ta  <->  et ) )  ->.  ( ( ph  \/  ch  \/  ta )  <->  ( ( ps  \/  th )  \/  et ) ) ).
9:?:  |-  ( ( ( ps  \/  th )  \/  et )  <->  ( ps  \/  th  \/  et ) )
10:8,9,?: e10 27600  |-  (. ( ( 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 27760 Virtual deduction proof of sbc3org 27431. 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_ 27532  |-  (. 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 27600  |-  (. A  e.  B  ->.  [. A  /  x ]. ( ( ( ph  \/  ps )  \/  ch )  <->  ( ph  \/  ps  \/  ch ) ) ).
4:1,33,?: e11 27593  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ( ph  \/  ps )  \/  ch )  <->  [. A  /  x ]. ( ph  \/  ps  \/  ch ) ) ).
5:2,4,?: e11 27593  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  \/  ps  \/  ch )  <->  ( [. A  /  x ]. ( ph  \/  ps )  \/  [. A  /  x ]. ch ) ) ).
6:1,?: e1_ 27532  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  \/  ps )  <->  ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps ) ) ).
7:6,?: e1_ 27532  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. ( ph  \/  ps )  \/  [. A  /  x ]. ch )  <->  ( ( [. A  /  x ]. ph  \/  [. A  /  x ]. ps )  \/  [. A  /  x ]. ch ) ) ).
8:5,7,?: e11 27593  |-  (. 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 27600  |-  (. 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 27761* Virtual deduction proof of alrim3con13v 27432. 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 27536  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ps ).
4:2,?: e2 27536  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ph ).
5:2,?: e2 27536  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ch ).
6:1,4,?: e12 27632  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ph ).
7:3,?: e2 27536  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ps ).
8:5,?: e2 27536  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  A. x ch ).
9:7,6,8,?: e222 27541  |-  (. ( ph  ->  A. x ph ) ,. ( ps  /\  ph  /\  ch )  ->.  ( A. x ps  /\  A. x ph  /\  A. x ch ) ).
10:9,?: e2 27536  |-  (. ( 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 27762 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 27632  |-  (. ( ( ph  /\  ps )  ->  ( ch  <->  th ) ) ,  ( ph  /\  ps )  ->.  ( ch  <->  th ) ).
6:3,5,?: e32 27666  |-  (. ( ( 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_ 27532  |-  (. ( ( 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 27763 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 27600  |-  (. ph  ->.  ( ps  ->  ( ch  <->  th ) ) ).
6:3,5,?: e21 27638  |-  (. ph ,. ps  ->.  ( ch  <->  th ) ).
7:4,6,?: e32 27666  |-  (. 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 27764* Virtual deduction proof of ra4sbc2 27433. 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 27656  |-  (. 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 27656  |-  (. 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 27663  |-  (. 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 27765 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 27600  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ( ph  /\  ps )  /\  ch )  ->  th ) ).
4:3,?: e1_ 27532  |-  (. ( ( ph  /\  ps  /\  ch )  ->  th )  ->.  ( ( ph  /\  ps )  ->  ( ch  ->  th ) ) ).
5:4,?: e1_ 27532  |-  (. ( ( 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_ 27532  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ph  /\  ps )  ->  ( ch  ->  th ) ) ).
9:8,?: e1_ 27532  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ( ph  /\  ps )  /\  ch )  ->  th ) ).
10:2,9,?: e01 27596  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  th ) ).
11:10:  |-  ( ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )  ->  ( ( ph  /\  ps  /\  ch )  ->  th ) )
qed:6,11,?: e00 27676  |-  ( ( ( 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 27766 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 27600  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
4:3,?: e1_ 27532  |-  (. ( ( 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_ 27532  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
8:7,2,?: e10 27600  |-  (. ( 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 27676  |-  ( ( ( 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 27767 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_ 27680  |-  ( 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 27768* Virtual deduction proof of sbcoreleleq 27434. 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_ 27532  |-  (. A  e.  B  ->.  ( [. A  /  y ]. x  e.  y  <->  x  e.  A ) ).
3:1,?: e1_ 27532  |-  (. A  e.  B  ->.  ( [. A  /  y ]. y  e.  x  <->  A  e.  x ) ).
4:1,?: e1_ 27532  |-  (. A  e.  B  ->.  ( [. A  /  y ]. x  =  y  <->  x  =  A ) ).
5:2,3,4,?: e111 27579  |-  (. 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_ 27532  |-  (. 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 27593  |-  (. 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 27769* Virtual deduction proof of nfra2 2572. 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 27676  |-  ( 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_ 27680  |-  ( 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 27676  |-  ( 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 27770* Virtual deduction proof of tratrb 27435. 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_ 27532  |-  (. ( 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_ 27532  |-  (. ( 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_ 27532  |-  (. ( 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 27536  |-  (. ( 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 27536  |-  (. ( 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 27561  |-  (. ( 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 27558  |-  (. ( 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 27540  |-  (. ( 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 27635  |-  (. ( 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 27663  |-  (. ( 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 27663  |-  (. ( 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 27635  |-  (. ( 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_ 27532  |-  (. ( 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 27561  |-  (. ( 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 27536  |-  (. ( 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 27632  |-  (. ( 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 27541  |-  (. ( 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_ 27680  |-  ( ( 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_ 27680  |-  ( ( 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_ 27532  |-  (. ( 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 27771 Virtual deduction proof of 3ax5 27436. 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_ 27532  |-  (. 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 27600  |-  (. 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 27772 Virtual deduction proof of syl5imp 27410. 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_ 27532  |-  (. ( ph  ->  ( ps  ->  ch ) )  ->.  ( ps  ->  ( ph  ->  ch ) ) ).
3::  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( th  ->  ps ) ).
4:3,2,?: e21 27638  |-  (. ( ph  ->  ( ps  ->  ch ) ) ,. ( th  ->  ps )  ->.  ( th  ->  ( ph  ->  ch ) ) ).
5:4,?: e2 27536  |-  (. ( 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 27773 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_ 27680  |-  ph
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ph   =>    |-  ph
 
TheoremancomsimpVD 27774 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_ 27680  |-  ( ( ( 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 27775* Quantification restricted to a subclass for two quantifiers. ssralv 3212 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 27430 is ssralv2VD 27775 without virtual deductions and was automatically derived from ssralv2VD 27775.
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 27776 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4386 using the Axiom of Regularity indirectly through dford2 7289. 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 27437 is ordelordALTVD 27776 without virtual deductions and was automatically derived from ordelordALTVD 27776 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 27777 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 3295 is equncomVD 27777 without virtual deductions and was automatically derived from equncomVD 27777.
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 27778 Inference form of equncom 3295. 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 3296 is equncomiVD 27778 without virtual deductions and was automatically derived from equncomiVD 27778.
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 27779 A set belongs to its successor. Alternate proof of sucid 4443. 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 27780 is sucidALTVD 27779 without virtual deductions and was automatically derived from sucidALTVD 27779. 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 4370, 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 7289.
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 27780 A set belongs to its successor. This proof was automatically derived from sucidALTVD 27779 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 27781 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 4443 is sucidVD 27781 without virtual deductions and was automatically derived from sucidVD 27781.
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 27782 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 27418 is imbi12VD 27782 without virtual deductions and was automatically derived from imbi12VD 27782.
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 27783 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 27419 is imbi13VD 27783 without virtual deductions and was automatically derived from imbi13VD 27783.
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 27784 Distribution of class substitution over a left-nested implication. Similar to sbcimg 3007. 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 27438 is sbcim2gVD 27784 without virtual deductions and was automatically derived from sbcim2gVD 27784.
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 27785 Implication form of sbcbiiOLD 3022. 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 27439 is sbcbiVD 27785 without virtual deductions and was automatically derived from sbcbiVD 27785.
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 27786* 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 27440 is trsbcVD 27786 without virtual deductions and was automatically derived from trsbcVD 27786.
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 27787* 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 27441 is truniALTVD 27787 without virtual deductions and was automatically derived from truniALTVD 27787.
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 27788 Non-virtual deduction form of e33 27642. 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 27420 is ee33VD 27788 without virtual deductions and was automatically derived from ee33VD 27788.
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 27789* The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 27790. 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 27790 is trintALTVD 27789 without virtual deductions and was automatically derived from trintALTVD 27789.
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 27790* The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 27790 is an alternative proof of trint 4102. trintALT 27790 is trintALTVD 27789 without virtual deductions and was automatically derived from trintALTVD 27789 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 27791 The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3404. 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 3404 is undif3VD 27791 without virtual deductions and was automatically derived from undif3VD 27791.
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 27792 Virtual deduction proof of sbcss 27442. 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 27442 is sbcssVD 27792 without virtual deductions and was automatically derived from sbcssVD 27792.
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 27793 Virtual deduction proof of csbing 3351. 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 3351 is csbingVD 27793 without virtual deductions and was automatically derived from csbingVD 27793.
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 27794* Virtual deduction proof of onfrALTlem5 27443. 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 27443 is onfrALTlem5VD 27794 without virtual deductions and was automatically derived from onfrALTlem5VD 27794.
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  =/=  (/)