P. 372 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

uunT11p2 37101

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 )

Theorem

uunT12 37102

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 )

Theorem

uunT12p1 37103

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 )

Theorem

uunT12p2 37104

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 )

Theorem

uunT12p3 37105

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 )

Theorem

uunT12p4 37106

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 )

Theorem

uunT12p5 37107

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 )

Theorem

uun111 37108

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 )

Theorem

3anidm12p1 37109

A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1321 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 )

Theorem

3anidm12p2 37110

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 )

Theorem

uun123 37111

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 )

Theorem

uun123p1 37112

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 )

Theorem

uun123p2 37113

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 )

Theorem

uun123p3 37114

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 )

Theorem

uun123p4 37115

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 )

Theorem

uun2221 37116

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 )

Theorem

uun2221p1 37117

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 )

Theorem

uun2221p2 37118

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 )

Theorem

3impdirp1 37119

A deduction unionizing a non-unionized collection of virtual hypotheses. Commuted version of 3impdir 1320. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ch /\ ps ) /\ ( ph /\ ps ) ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )

Theorem

3impcombi 37120

A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017.)

|- ( ( ph /\ ps /\ ph ) -> ( ch <-> th ) )   =>    |- ( ( ps /\ ph /\ ch ) -> th )

Theorem

3imp231 37121

Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)

|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ps /\ ch /\ ph ) -> th )

21.29.6  Theorems proved using Virtual Deduction

Theorem

trsspwALT 37122

Virtual deduction proof of the left-to-right implication of dftr4 4461. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 4461 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> A C_ ~P A )

Theorem

trsspwALT2 37123

Virtual deduction proof of trsspwALT 37122. This proof is the same as the proof of trsspwALT 37122 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 )

Theorem

trsspwALT3 37124

Short predicate calculus proof of the left-to-right implication of dftr4 4461. 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 37123, which is the virtual deduction proof trsspwALT 37122 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> A C_ ~P A )

Theorem

sspwtr 37125

Virtual deduction proof of the right-to-left implication of dftr4 4461. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 37125 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A C_ ~P A -> Tr A )

Theorem

sspwtrALT 37126

Virtual deduction proof of sspwtr 37125. This proof is the same as the proof of sspwtr 37125 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 )

Theorem

csbabgOLD 37127*

Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) Obsolete as of 19-Aug-2018. Use csbab 3765 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> [_ A / x ]_ { y | ph } = { y | [. A / x ]. ph } )

Theorem

csbunigOLD 37128

Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 22-Aug-2018. Use csbuni 4185 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B )

Theorem

csbfv12gALTOLD 37129

Move class substitution in and out of a function value. The proof is derived from the virtual deduction proof csbfv12gALTVD 37212. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 5855 instead. (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) )

Theorem

csbxpgOLD 37130

Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbrn 5254 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. D -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )

Theorem

csbingOLD 37131

Distribute proper substitution through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) Obsolete as of 18-Aug-2018. Use csbin 3767 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. B -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) )

Theorem

csbresgOLD 37132

Distribute proper substitution through the restriction of a class. csbresgOLD 37132 is derived from the virtual deduction proof csbresgVD 37208. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbres 5065 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) )

Theorem

csbrngOLD 37133

Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbrn 5254 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> [_ A / x ]_ ran B = ran [_ A / x ]_ B )

Theorem

csbima12gALTOLD 37134

Move class substitution in and out of the image of a function. The proof is derived from the virtual deduction proof csbima12gALTVD 37210. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 5855 instead. (Proof modification is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. C -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )

Theorem

sspwtrALT2 37135

Short predicate calculus proof of the right-to-left implication of dftr4 4461. 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 37126, which is the virtual deduction proof sspwtr 37125 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A C_ ~P A -> Tr A )

Theorem

pwtrVD 37136

Virtual deduction proof of pwtr 4612; see pwtrrVD 37137 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> Tr ~P A )

Theorem

pwtrrVD 37137

Virtual deduction proof of pwtr 4612; see pwtrVD 37136 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- A e. _V   =>    |- ( Tr ~P A -> Tr A )

Theorem

suctrALT 37138

The successor of a transitive class is transitive. The proof of http://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT 37138 using completeusersproof, which is verified by the Metamath program. The proof of http://us.metamath.org/other/completeusersproof/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr 5463 for the original proof. (Contributed by Alan Sare, 11-Apr-2009.) (Revised by Alan Sare, 12-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> Tr suc A )

Theorem

snssiALTVD 37139

Virtual deduction proof of snssiALT 37140. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> { A } C_ B )

Theorem

snssiALT 37140

If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 4082. This theorem was automatically generated from snssiALTVD 37139 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 )

Theorem

snsslVD 37141

Virtual deduction proof of snssl 37142. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- A e. _V   =>    |- ( { A } C_ B -> A e. B )

Theorem

snssl 37142

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 4062. The proof of this theorem was automatically generated from snsslVD 37141 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 )

Theorem

snelpwrVD 37143

Virtual deduction proof of snelpwi 4604. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> { A } e. ~P B )

Theorem

unipwrVD 37144

Virtual deduction proof of unipwr 37145. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- A C_ U. ~P A

Theorem

unipwr 37145

A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 4609. The proof of this theorem was automatically generated from unipwrVD 37144 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

Theorem

sstrALT2VD 37146

Virtual deduction proof of sstrALT2 37147. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( A C_ B /\ B C_ C ) -> A C_ C )

Theorem

sstrALT2 37147

Virtual deduction proof of sstr 3410, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 37146 using the command file translate_without_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 )

Theorem

suctrALT2VD 37148

Virtual deduction proof of suctrALT2 37149. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> Tr suc A )

Theorem

suctrALT2 37149

Virtual deduction proof of suctr 5463. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 37148 using the tools command file translate_without_overwriting_minimize_excluding_duplicates.cmd . (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( Tr A -> Tr suc A )

Theorem

elex2VD 37150*

Virtual deduction proof of elex2 3029. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> E. x x e. B )

Theorem

elex22VD 37151*

Virtual deduction proof of elex22 3030. (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 ) )

Theorem

eqsbc3rVD 37152*

Virtual deduction proof of eqsbc3r 3294. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> ( [. A / x ]. C = x <-> C = A ) )

Theorem

zfregs2VD 37153*

Virtual deduction proof of zfregs2 8164. (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 ) )

Theorem

tpid3gVD 37154

Virtual deduction proof of tpid3g 4053. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( A e. B -> A e. { C , D , A } )

Theorem

en3lplem1VD 37155*

Virtual deduction proof of en3lplem1 8067. (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 ) ) )

Theorem

en3lplem2VD 37156*

Virtual deduction proof of en3lplem2 8068. (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 ) ) )

Theorem

en3lpVD 37157

Virtual deduction proof of en3lp 8069. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- -. ( A e. B /\ B e. C /\ C e. A )

21.29.7  Theorems proved using Virtual Deduction with mmj2 assistance

Theorem

simplbi2VD 37158

Virtual deduction proof of simplbi2 629. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	|- ( ph <-> ( ps /\ ch ) )
3:1,?: e0a 37075	|- ( ( ps /\ ch ) -> ph )
qed:3,?: e0a 37075	|- ( ps -> ( ch -> ph ) )

The proof of simplbi2 629 was automatically derived from it. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch -> ph ) )

Theorem

3ornot23VD 37159

Virtual deduction proof of 3ornot23 36778. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::

|- (. ( -. ph /\ -. ps ) ->. ( -. ph /\ -. ps ) ).
2::	|- (. ( -. ph /\ -. ps ) ,. ( ch \/ ph \/ ps ) ->. ( ch \/ ph \/ ps ) ).
3:1,?: e1a 36920	|- (. ( -. ph /\ -. ps ) ->. -. ph ).
4:1,?: e1a 36920	|- (. ( -. ph /\ -. ps ) ->. -. ps ).
5:3,4,?: e11 36981	|- (. ( -. ph /\ -. ps ) ->. -. ( ph \/ ps ) ).
6:2,?: e2 36924	|- (. ( -. ph /\ -. ps ) ,. ( ch \/ ph \/ ps ) ->. ( ch \/ ( ph \/ ps ) ) ).
7:5,6,?: e12 37027	|- (. ( -. 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 ) )

Theorem

orbi1rVD 37160

Virtual deduction proof of orbi1r 36779. 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 36924	|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ph \/ ch ) ).
4:1,3,?: e12 37027	|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ps \/ ch ) ).
5:4,?: e2 36924	|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ch \/ ps ) ).
6:5:	|- (. ( ph <-> ps ) ->. ( ( ch \/ ph ) -> ( ch \/ ps ) ) ).
7::	|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ch \/ ps ) ).
8:7,?: e2 36924	|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ps \/ ch ) ).
9:1,8,?: e12 37027	|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ph \/ ch ) ).
10:9,?: e2 36924	|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ch \/ ph ) ).
11:10:	|- (. ( ph <-> ps ) ->. ( ( ch \/ ps ) -> ( ch \/ ph ) ) ).
12:6,11,?: e11 36981	|- (. ( 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 ) ) )

Theorem

bitr3VD 37161

Virtual deduction proof of bitr3 36780. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ph <-> ps ) ->. ( ph <-> ps ) ).
2:1,?: e1a 36920	|- (. ( ph <-> ps ) ->. ( ps <-> ph ) ).
3::	|- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ph <-> ch ) ).
4:3,?: e2 36924	|- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ch <-> ph ) ).
5:2,4,?: e12 37027	|- (. ( 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 ) ) )

Theorem

3orbi123VD 37162

Virtual deduction proof of 3orbi123 36781. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ).
2:1,?: e1a 36920	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ph <-> ps ) ).
3:1,?: e1a 36920	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ch <-> th ) ).
4:1,?: e1a 36920	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ta <-> et ) ).
5:2,3,?: e11 36981	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch ) <-> ( ps \/ th ) ) ).
6:5,4,?: e11 36981	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
7:?:	|- ( ( ( ph \/ ch ) \/ ta ) <-> ( ph \/ ch \/ ta ) )
8:6,7,?: e10 36987	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
9:?:	|- ( ( ( ps \/ th ) \/ et ) <-> ( ps \/ th \/ et ) )
10:8,9,?: e10 36987	|- (. ( ( 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 ) ) )

Theorem

sbc3orgVD 37163

Virtual deduction proof of sbc3orgOLD 36806. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. A e. B ->. A e. B ).
2:1,?: e1a 36920	|- (. 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 36987	|- (. A e. B ->. [. A / x ]. ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) ) ).
4:1,33,?: e11 36981	|- (. A e. B ->. ( [. A / x ]. ( ( ph \/ ps ) \/ ch ) <-> [. A / x ]. ( ph \/ ps \/ ch ) ) ).
5:2,4,?: e11 36981	|- (. A e. B ->. ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) ) ).
6:1,?: e1a 36920	|- (. A e. B ->. ( [. A / x ]. ( ph \/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) ) ).
7:6,?: e1a 36920	|- (. A e. B ->. ( ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) ) ).
8:5,7,?: e11 36981	|- (. 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 36987	|- (. 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 ) ) )

Theorem

19.21a3con13vVD 37164*

Virtual deduction proof of alrim3con13v 36807. 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 36924	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ps ).
4:2,?: e2 36924	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ph ).
5:2,?: e2 36924	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ch ).
6:1,4,?: e12 37027	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ph ).
7:3,?: e2 36924	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ps ).
8:5,?: e2 36924	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. A. x ch ).
9:7,6,8,?: e222 36929	|- (. ( ph -> A. x ph ) ,. ( ps /\ ph /\ ch ) ->. ( A. x ps /\ A. x ph /\ A. x ch ) ).
10:9,?: e2 36924	|- (. ( 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 ) ) )

Theorem

exbirVD 37165

Virtual deduction proof of exbir 36746. 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 37027	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) ->. ( ch <-> th ) ).
6:3,5,?: e32 37061	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) , th ->. ch ).
7:6:	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) ->. ( th -> ch ) ).
8:7:	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) ->. ( ( ph /\ ps ) -> ( th -> ch ) ) ).
9:8,?: e1a 36920	|- (. ( ( 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 ) ) ) )

Theorem

exbiriVD 37166

Virtual deduction proof of exbiri 626. 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 36987	|- (. ph ->. ( ps -> ( ch <-> th ) ) ).
6:3,5,?: e21 37033	|- (. ph ,. ps ->. ( ch <-> th ) ).
7:4,6,?: e32 37061	|- (. 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 ) ) )

Theorem

rspsbc2VD 37167*

Virtual deduction proof of rspsbc2 36808. 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 37051	|- (. 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 37051	|- (. 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 37058	|- (. 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 ) ) )

Theorem

3impexpVD 37168

Virtual deduction proof of 3impexp 1227. 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 36987	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ( ph /\ ps ) /\ ch ) -> th ) ).
4:3,?: e1a 36920	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ph /\ ps ) -> ( ch -> th ) ) ).
5:4,?: e1a 36920	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ph -> ( ps -> ( ch -> th ) ) ) ).
6:5:	|- ( ( ( ph /\ ps /\ ch ) -> th ) -> ( ph -> ( ps -> ( ch -> th ) ) ) )
7::	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ph -> ( ps -> ( ch -> th ) ) ) ).
8:7,?: e1a 36920	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ph /\ ps ) -> ( ch -> th ) ) ).
9:8,?: e1a 36920	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ( ph /\ ps ) /\ ch ) -> th ) ).
10:2,9,?: e01 36984	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ph /\ ps /\ ch ) -> th ) ).
11:10:	|- ( ( ph -> ( ps -> ( ch -> th ) ) ) -> ( ( ph /\ ps /\ ch ) -> th ) )
qed:6,11,?: e00 37071	|- ( ( ( 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 ) ) ) )

Theorem

3impexpbicomVD 37169

Virtual deduction proof of 3impexpbicom 36747. 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 36987	|- (. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ->. ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ).
4:3,?: e1a 36920	|- (. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ->. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ).
5:4:	|- ( ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) -> ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) )
6::	|- (. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ->. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ).
7:6,?: e1a 36920	|- (. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ->. ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ).
8:7,2,?: e10 36987	|- (. ( 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 37071	|- ( ( ( 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 ) ) ) ) )

Theorem

3impexpbicomiVD 37170

Virtual deduction proof of 3impexpbicomi 36748. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	|- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) )
qed:1,?: e0a 37075	|- ( 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 ) ) ) )

Theorem

sbcel1gvOLD 37171*

Class substitution into a membership relation. (Contributed by NM, 17-Nov-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) Obsolete as of 17-Aug-2018. Use sbcel1v 3296 instead. (New usage is discouraged.) (Proof modification is discouraged.)

|- ( A e. V -> ( [. A / x ]. x e. B <-> A e. B ) )

Theorem

sbcoreleleqVD 37172*

Virtual deduction proof of sbcoreleleq 36809. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. A e. B ->. A e. B ).
2:1,?: e1a 36920	|- (. A e. B ->. ( [. A / y ]. x e. y <-> x e. A ) ).
3:1,?: e1a 36920	|- (. A e. B ->. ( [. A / y ]. y e. x <-> A e. x ) ).
4:1,?: e1a 36920	|- (. A e. B ->. ( [. A / y ]. x = y <-> x = A ) ).
5:2,3,4,?: e111 36967	|- (. A e. B ->. ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
6:1,?: e1a 36920	|- (. 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 36981	|- (. 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 ) ) )

Theorem

hbra2VD 37173*

Virtual deduction proof of nfra2 2747. 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 37071	|- ( A. x e. A A. y e. B ph -> A. y A. y e. B A. x e. A ph )
4:2:	|- A. y ( A. x e. A A. y e. B ph <-> A. y e. B A. x e. A ph )
5:4,?: e0a 37075	|- ( 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 37071	|- ( 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 )

Theorem

tratrbVD 37174*

Virtual deduction proof of tratrb 36810. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ).
2:1,?: e1a 36920	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. Tr A ).
3:1,?: e1a 36920	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
4:1,?: e1a 36920	|- (. ( 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 36924	|- (. ( 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 36924	|- (. ( 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 36949	|- (. ( 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 36946	|- (. ( 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 36928	|- (. ( 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 37030	|- (. ( 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 37058	|- (. ( 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 37058	|- (. ( 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 37030	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. -. x = B ).
21:3,?: e1a 36920	|- (. ( 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 36949	|- (. ( 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 36924	|- (. ( 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 37027	|- (. ( 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 36929	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. B ).
26:25:	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. ( ( x e. y /\ y e. B ) -> x e. B ) ).
27::	|- ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> A. y A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
28:27,?: e0a 37075	|- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> A. y ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) )
29:28,26:	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. y ( ( x e. y /\ y e. B ) -> x e. B ) ).
30::	|- ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> A. x A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
31:30,?: e0a 37075	|- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> A. x ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) )
32:31,29:	|- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. x A. y ( ( x e. y /\ y e. B ) -> x e. B ) ).
33:32,?: e1a 36920	|- (. ( 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 )

Theorem

al2imVD 37175

Virtual deduction proof of al2im 1680. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. A. x ( ph -> ( ps -> ch ) ) ->. A. x ( ph -> ( ps -> ch ) ) ).
2:1,?: e1a 36920	|- (. 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 36987	|- (. 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 ) ) )

Theorem

syl5impVD 37176

Virtual deduction proof of syl5imp 36782. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- (. ( ph -> ( ps -> ch ) ) ->. ( ph -> ( ps -> ch ) ) ).
2:1,?: e1a 36920	|- (. ( ph -> ( ps -> ch ) ) ->. ( ps -> ( ph -> ch ) ) ).
3::	|- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( th -> ps ) ).
4:3,2,?: e21 37033	|- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( th -> ( ph -> ch ) ) ).
5:4,?: e2 36924	|- (. ( 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 ) ) ) )

Theorem

idiVD 37177

Virtual deduction proof of idiALT 36745. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	|- ph
qed:1,?: e0a 37075	|- ph

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ph   =>    |- ph

Theorem

ancomstVD 37178

Closed form of ancoms 454. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	|- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
qed:1,?: e0a 37075	|- ( ( ( ph /\ ps ) -> ch ) <-> ( ( ps /\ ph ) -> ch ) )

The proof of ancomst 453 is derived automatically from it. (Contributed by Alan Sare, 25-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ( ph /\ ps ) -> ch ) <-> ( ( ps /\ ph ) -> ch ) )

Theorem

ssralv2VD 37179*

Quantification restricted to a subclass for two quantifiers. ssralv 3463 for two quantifiers. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ssralv2 36801 is ssralv2VD 37179 without virtual deductions and was automatically derived from ssralv2VD 37179.

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 ) )

Theorem

ordelordALTVD 37180

An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 5402 using the Axiom of Regularity indirectly through dford2 8073. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that _E Fr A because this is inferred by the Axiom of Regularity. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ordelordALT 36811 is ordelordALTVD 37180 without virtual deductions and was automatically derived from ordelordALTVD 37180 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 )

Theorem

equncomVD 37181

If a class equals the union of two other classes, then it equals the union of those two classes commuted. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. equncom 3549 is equncomVD 37181 without virtual deductions and was automatically derived from equncomVD 37181.

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 ) )

Theorem

equncomiVD 37182

Inference form of equncom 3549. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. equncomi 3550 is equncomiVD 37182 without virtual deductions and was automatically derived from equncomiVD 37182.

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 )

Theorem

sucidALTVD 37183

A set belongs to its successor. Alternate proof of sucid 5459. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sucidALT 37184 is sucidALTVD 37183 without virtual deductions and was automatically derived from sucidALTVD 37183. 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 5386, a reference definition (axiom) in set.mm. Also, a theorem or deduction is said to be a semantic variation of another theorem or deduction if it is obvious upon cursory inspection that it has the same meaning as a weaker form of the latter theorem or deduction. For example, the deduction Ord A infers A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) is a semantic variation of the theorem ( Ord A <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) ), which unifies with the set.mm reference definition (axiom) dford2 8073.

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

Theorem

sucidALT 37184

A set belongs to its successor. This proof was automatically derived from sucidALTVD 37183 using translate_without_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

Theorem

sucidVD 37185

A set belongs to its successor. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sucid 5459 is sucidVD 37185 without virtual deductions and was automatically derived from sucidVD 37185.

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

Theorem

imbi12VD 37186

Implication form of imbi12i 327. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi12 323 is imbi12VD 37186 without virtual deductions and was automatically derived from imbi12VD 37186.

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 ) ) ) )

Theorem

imbi13VD 37187

Join three logical equivalences to form equivalence of implications. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi13 36790 is imbi13VD 37187 without virtual deductions and was automatically derived from imbi13VD 37187.

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 ) ) ) ) ) )

Theorem

sbcim2gVD 37188

Distribution of class substitution over a left-nested implication. Similar to sbcimg 3279. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcim2g 36812 is sbcim2gVD 37188 without virtual deductions and was automatically derived from sbcim2gVD 37188.

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 ) ) ) )

Theorem

sbcbiVD 37189

Implication form of sbcbiiOLD 36805. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcbi 36813 is sbcbiVD 37189 without virtual deductions and was automatically derived from sbcbiVD 37189.

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 ) ) )

Theorem

trsbcVD 37190*

Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc 36814 is trsbcVD 37190 without virtual deductions and was automatically derived from trsbcVD 37190.

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 ) )

Theorem

truniALTVD 37191*

The union of a class of transitive sets is transitive. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. truniALT 36815 is truniALTVD 37191 without virtual deductions and was automatically derived from truniALTVD 37191.

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 )

Theorem

ee33VD 37192

Non-virtual deduction form of e33 37037. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ee33 36791 is ee33VD 37192 without virtual deductions and was automatically derived from ee33VD 37192.

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 ) ) )

Theorem

trintALTVD 37193*

The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 37194. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trintALT 37194 is trintALTVD 37193 without virtual deductions and was automatically derived from trintALTVD 37193.

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 )

Theorem

trintALT 37194*

The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 37194 is an alternate proof of trint 4471. trintALT 37194 is trintALTVD 37193 without virtual deductions and was automatically derived from trintALTVD 37193 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 )

Theorem

undif3VD 37195

The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3672. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. undif3 3672 is undif3VD 37195 without virtual deductions and was automatically derived from undif3VD 37195.

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 ) )

Theorem

sbcssgVD 37196

Virtual deduction proof of sbcssg 3848. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcssg 3848 is sbcssgVD 37196 without virtual deductions and was automatically derived from sbcssgVD 37196.

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 ) )

Theorem

csbingVD 37197

Virtual deduction proof of csbingOLD 37131. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbingOLD 37131 is csbingVD 37197 without virtual deductions and was automatically derived from csbingVD 37197.

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 ) )

Theorem

onfrALTlem5VD 37198*

Virtual deduction proof of onfrALTlem5 36821. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem5 36821 is onfrALTlem5VD 37198 without virtual deductions and was automatically derived from onfrALTlem5VD 37198.

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: