P. 373 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

unipwrVD 37201

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

|- A C_ U. ~P A

Theorem

unipwr 37202

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

Virtual deduction proof of sstrALT2 37204. (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 37204

Virtual deduction proof of sstr 3472, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 37203 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 37205

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

|- ( Tr A -> Tr suc A )

Theorem

suctrALT2 37206

Virtual deduction proof of suctr 5525. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 37205 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 37207*

Virtual deduction proof of elex2 3092. (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 37208*

Virtual deduction proof of elex22 3093. (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 37209*

Virtual deduction proof of eqsbc3r 3356. (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 37210*

Virtual deduction proof of zfregs2 8225. (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 37211

Virtual deduction proof of tpid3g 4115. (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 37212*

Virtual deduction proof of en3lplem1 8128. (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 37213*

Virtual deduction proof of en3lplem2 8129. (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 37214

Virtual deduction proof of en3lp 8130. (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 37215

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 37132	|- ( ( ps /\ ch ) -> ph )
qed:3,?: e0a 37132	|- ( 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 37216

Virtual deduction proof of 3ornot23 36835. 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 36977	|- (. ( -. ph /\ -. ps ) ->. -. ph ).
4:1,?: e1a 36977	|- (. ( -. ph /\ -. ps ) ->. -. ps ).
5:3,4,?: e11 37038	|- (. ( -. ph /\ -. ps ) ->. -. ( ph \/ ps ) ).
6:2,?: e2 36981	|- (. ( -. ph /\ -. ps ) ,. ( ch \/ ph \/ ps ) ->. ( ch \/ ( ph \/ ps ) ) ).
7:5,6,?: e12 37084	|- (. ( -. 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 37217

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

Virtual deduction proof of bitr3 36837. 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 36977	|- (. ( ph <-> ps ) ->. ( ps <-> ph ) ).
3::	|- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ph <-> ch ) ).
4:3,?: e2 36981	|- (. ( ph <-> ps ) ,. ( ph <-> ch ) ->. ( ch <-> ph ) ).
5:2,4,?: e12 37084	|- (. ( 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 37219

Virtual deduction proof of 3orbi123 36838. 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 36977	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ph <-> ps ) ).
3:1,?: e1a 36977	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ch <-> th ) ).
4:1,?: e1a 36977	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ta <-> et ) ).
5:2,3,?: e11 37038	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch ) <-> ( ps \/ th ) ) ).
6:5,4,?: e11 37038	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ( ph \/ ch ) \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
7:?:	|- ( ( ( ph \/ ch ) \/ ta ) <-> ( ph \/ ch \/ ta ) )
8:6,7,?: e10 37044	|- (. ( ( ph <-> ps ) /\ ( ch <-> th ) /\ ( ta <-> et ) ) ->. ( ( ph \/ ch \/ ta ) <-> ( ( ps \/ th ) \/ et ) ) ).
9:?:	|- ( ( ( ps \/ th ) \/ et ) <-> ( ps \/ th \/ et ) )
10:8,9,?: e10 37044	|- (. ( ( 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 37220

Virtual deduction proof of sbc3orgOLD 36863. 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 36977	|- (. 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 37044	|- (. A e. B ->. [. A / x ]. ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) ) ).
4:1,33,?: e11 37038	|- (. A e. B ->. ( [. A / x ]. ( ( ph \/ ps ) \/ ch ) <-> [. A / x ]. ( ph \/ ps \/ ch ) ) ).
5:2,4,?: e11 37038	|- (. A e. B ->. ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) ) ).
6:1,?: e1a 36977	|- (. A e. B ->. ( [. A / x ]. ( ph \/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) ) ).
7:6,?: e1a 36977	|- (. A e. B ->. ( ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) ) ).
8:5,7,?: e11 37038	|- (. 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 37044	|- (. 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 37221*

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

Virtual deduction proof of exbir 36803. 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 37084	|- (. ( ( ph /\ ps ) -> ( ch <-> th ) ) , ( ph /\ ps ) ->. ( ch <-> th ) ).
6:3,5,?: e32 37118	|- (. ( ( 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 36977	|- (. ( ( 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 37223

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 37044	|- (. ph ->. ( ps -> ( ch <-> th ) ) ).
6:3,5,?: e21 37090	|- (. ph ,. ps ->. ( ch <-> th ) ).
7:4,6,?: e32 37118	|- (. 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 37224*

Virtual deduction proof of rspsbc2 36865. 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 37108	|- (. 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 37108	|- (. 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 37115	|- (. 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 37225

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 37044	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ( ph /\ ps ) /\ ch ) -> th ) ).
4:3,?: e1a 36977	|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ph /\ ps ) -> ( ch -> th ) ) ).
5:4,?: e1a 36977	|- (. ( ( 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 36977	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ph /\ ps ) -> ( ch -> th ) ) ).
9:8,?: e1a 36977	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ( ph /\ ps ) /\ ch ) -> th ) ).
10:2,9,?: e01 37041	|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ph /\ ps /\ ch ) -> th ) ).
11:10:	|- ( ( ph -> ( ps -> ( ch -> th ) ) ) -> ( ( ph /\ ps /\ ch ) -> th ) )
qed:6,11,?: e00 37128	|- ( ( ( 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 37226

Virtual deduction proof of 3impexpbicom 36804. 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 37044	|- (. ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) ->. ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ).
4:3,?: e1a 36977	|- (. ( ( 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 36977	|- (. ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) ->. ( ( ph /\ ps /\ ch ) -> ( ta <-> th ) ) ).
8:7,2,?: e10 37044	|- (. ( 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 37128	|- ( ( ( 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 37227

Virtual deduction proof of 3impexpbicomi 36805. 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 37132	|- ( 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 37228*

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 3358 instead. (New usage is discouraged.) (Proof modification is discouraged.)

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

Theorem

sbcoreleleqVD 37229*

Virtual deduction proof of sbcoreleleq 36866. 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 36977	|- (. A e. B ->. ( [. A / y ]. x e. y <-> x e. A ) ).
3:1,?: e1a 36977	|- (. A e. B ->. ( [. A / y ]. y e. x <-> A e. x ) ).
4:1,?: e1a 36977	|- (. A e. B ->. ( [. A / y ]. x = y <-> x = A ) ).
5:2,3,4,?: e111 37024	|- (. 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 36977	|- (. 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 37038	|- (. 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 37230*

Virtual deduction proof of nfra2 2809. 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 37128	|- ( 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 37132	|- ( 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 37128	|- ( 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 37231*

Virtual deduction proof of tratrb 36867. 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 36977	|- (. ( 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 36977	|- (. ( 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 36977	|- (. ( 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 36981	|- (. ( 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 36981	|- (. ( 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 37006	|- (. ( 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 37003	|- (. ( 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 36985	|- (. ( 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 37087	|- (. ( 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 37115	|- (. ( 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 37115	|- (. ( 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 37087	|- (. ( 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 36977	|- (. ( 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 37006	|- (. ( 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 36981	|- (. ( 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 37084	|- (. ( 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 36986	|- (. ( 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 37132	|- ( ( 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 37132	|- ( ( 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 36977	|- (. ( 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 37232

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 36977	|- (. 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 37044	|- (. 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 37233

Virtual deduction proof of syl5imp 36839. 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 36977	|- (. ( ph -> ( ps -> ch ) ) ->. ( ps -> ( ph -> ch ) ) ).
3::	|- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( th -> ps ) ).
4:3,2,?: e21 37090	|- (. ( ph -> ( ps -> ch ) ) ,. ( th -> ps ) ->. ( th -> ( ph -> ch ) ) ).
5:4,?: e2 36981	|- (. ( 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 37234

Virtual deduction proof of idiALT 36802. 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 37132	|- ph

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

|- ph   =>    |- ph

Theorem

ancomstVD 37235

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 37132	|- ( ( ( 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 37236*

Quantification restricted to a subclass for two quantifiers. ssralv 3525 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 36858 is ssralv2VD 37236 without virtual deductions and was automatically derived from ssralv2VD 37236.

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 37237

An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 5464 using the Axiom of Regularity indirectly through dford2 8134. 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 36868 is ordelordALTVD 37237 without virtual deductions and was automatically derived from ordelordALTVD 37237 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 37238

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 3611 is equncomVD 37238 without virtual deductions and was automatically derived from equncomVD 37238.

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 37239

Inference form of equncom 3611. 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 3612 is equncomiVD 37239 without virtual deductions and was automatically derived from equncomiVD 37239.

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 37240

A set belongs to its successor. Alternate proof of sucid 5521. 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 37241 is sucidALTVD 37240 without virtual deductions and was automatically derived from sucidALTVD 37240. 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 5448, 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 8134.

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 37241

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

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 5521 is sucidVD 37242 without virtual deductions and was automatically derived from sucidVD 37242.

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 37243

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 37243 without virtual deductions and was automatically derived from imbi12VD 37243.

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 37244

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 36847 is imbi13VD 37244 without virtual deductions and was automatically derived from imbi13VD 37244.

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 37245

Distribution of class substitution over a left-nested implication. Similar to sbcimg 3341. 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 36869 is sbcim2gVD 37245 without virtual deductions and was automatically derived from sbcim2gVD 37245.

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 37246

Implication form of sbcbiiOLD 36862. 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 36870 is sbcbiVD 37246 without virtual deductions and was automatically derived from sbcbiVD 37246.

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 37247*

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 36871 is trsbcVD 37247 without virtual deductions and was automatically derived from trsbcVD 37247.

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 37248*

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 36872 is truniALTVD 37248 without virtual deductions and was automatically derived from truniALTVD 37248.

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 37249

Non-virtual deduction form of e33 37094. 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 36848 is ee33VD 37249 without virtual deductions and was automatically derived from ee33VD 37249.

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 37250*

The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 37251. 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 37251 is trintALTVD 37250 without virtual deductions and was automatically derived from trintALTVD 37250.

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 37251*

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

The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3734. 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 3734 is undif3VD 37252 without virtual deductions and was automatically derived from undif3VD 37252.

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 37253

Virtual deduction proof of sbcssg 3910. 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 3910 is sbcssgVD 37253 without virtual deductions and was automatically derived from sbcssgVD 37253.

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 37254

Virtual deduction proof of csbingOLD 37188. 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 37188 is csbingVD 37254 without virtual deductions and was automatically derived from csbingVD 37254.

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 37255*

Virtual deduction proof of onfrALTlem5 36878. 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 36878 is onfrALTlem5VD 37255 without virtual deductions and was automatically derived from onfrALTlem5VD 37255.

1::	|- a e. _V
2:1:	|- ( a i^i x ) e. _V
3:2:	|- ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) )
4:3:	|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> -. ( a i^i x ) = (/) )
5::	|- ( ( a i^i x ) =/= (/) <-> -. ( a i^i x ) = (/) )
6:4,5:	|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) =/= (/) )
7:2:	|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
8::	|- ( b =/= (/) <-> -. b = (/) )
9:8:	|- A. b ( b =/= (/) <-> -. b = (/) )
10:2,9:	|- ( [. ( a i^i x ) / b ]. b =/= (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
11:7,10:	|- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. b =/= (/) )
12:6,11:	|- ( [. ( a i^i x ) / b ]. b =/= (/) <-> ( a i^i x ) =/= (/) )
13:2:	|- ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) )
14:12,13:	|- ( ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
15:2:	|- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) )
16:15,14:	|- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
17:2:	|- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y )
18:2:	|- [_ ( a i^i x ) / b ]_ b = ( a i^i x )
19:2:	|- [_ ( a i^i x ) / b ]_ y = y
20:18,19:	|- ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) = ( ( a i^i x ) i^i y )
21:17,20:	|- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( ( a i^i x ) i^i y )
22:2:	|- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) )
23:2:	|- [_ ( a i^i x ) / b ]_ (/) = (/)
24:21,23:	|- ( [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) <-> ( ( a i^i x ) i^i y ) = (/) )
25:22,24:	|- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> ( ( a i^i x ) i^i y ) = (/) )
26:2:	|- ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) )
27:25,26:	|- ( ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
28:2:	|- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) )
29:27,28:	|- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
30:29:	|- A. y ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
31:30:	|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
32::	|- ( E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
33:31,32:	|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
34:2:	|- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
35:33,34:	|- ( [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
36::	|- ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
37:36:	|- A. b ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
38:2,37:	|- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
39:35,38:	|- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
40:16,39:	|- ( ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
41:2:	|- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) )
qed:40,41:	|- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )

(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i