P. 374 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

idiVD 37301

Virtual deduction proof of idiALT 36876. 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 37199	|- ph

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

|- ph   =>    |- ph

Theorem

ancomstVD 37302

Closed form of ancoms 459. 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 37199	|- ( ( ( ph /\ ps ) -> ch ) <-> ( ( ps /\ ph ) -> ch ) )

The proof of ancomst 458 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 37303*

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

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 37304

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 8151. 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 36942 is ordelordALTVD 37304 without virtual deductions and was automatically derived from ordelordALTVD 37304 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 37305

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

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 37306

Inference form of equncom 3591. 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 3592 is equncomiVD 37306 without virtual deductions and was automatically derived from equncomiVD 37306.

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 37307

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 37308 is sucidALTVD 37307 without virtual deductions and was automatically derived from sucidALTVD 37307. 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 8151.

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 37308

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

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

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 37310

Implication form of imbi12i 332. 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 328 is imbi12VD 37310 without virtual deductions and was automatically derived from imbi12VD 37310.

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 37311

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

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 37312

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

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 37313

Implication form of sbcbiiOLD 36936. 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 36944 is sbcbiVD 37313 without virtual deductions and was automatically derived from sbcbiVD 37313.

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

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

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

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

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 37316

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

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

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

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

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

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

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 37320

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

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 37321

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

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

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

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

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

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

Theorem

onfrALTlem4VD 37323*

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

1::	|- y e. _V
2:1:	|- ( [. y / x ]. ( a i^i x ) = (/) <-> [_ y / x ]_ ( a i^i x ) = [_ y / x ]_ (/) )
3:1:	|- [_ y / x ]_ ( a i^i x ) = ( [_ y / x ]_ a i^i [_ y / x ]_ x )
4:1:	|- [_ y / x ]_ a = a
5:1:	|- [_ y / x ]_ x = y
6:4,5:	|- ( [_ y / x ]_ a i^i [_ y / x ]_ x ) = ( a i^i y )
7:3,6:	|- [_ y / x ]_ ( a i^i x ) = ( a i^i y )
8:1:	|- [_ y / x ]_ (/) = (/)
9:7,8:	|- ( [_ y / x ]_ ( a i^i x ) = [_ y / x ]_ (/) <-> ( a i^i y ) = (/) )
10:2,9:	|- ( [. y / x ]. ( a i^i x ) = (/) <-> ( a i^i y ) = (/) )
11:1:	|- ( [. y / x ]. x e. a <-> y e. a )
12:11,10:	|- ( ( [. y / x ]. x e. a /\ [. y / x ]. ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )
13:1:	|- ( [. y / x ]. ( x e. a /\ ( a i^i x ) = (/) ) <-> ( [. y / x ]. x e. a /\ [. y / x ]. ( a i^i x ) = (/) ) )
qed:13,12:	|- ( [. y / x ]. ( x e. a /\ ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )

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

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

Theorem

onfrALTlem3VD 37324*

Virtual deduction proof of onfrALTlem3 36954. 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. onfrALTlem3 36954 is onfrALTlem3VD 37324 without virtual deductions and was automatically derived from onfrALTlem3VD 37324.

1::	|- (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
2::	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
3:2:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
4:1:	|- (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
5:3,4:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
6:5:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
7:6:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. _E We x ).
8::	|- ( a i^i x ) C_ x
9:7,8:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. _E We ( a i^i x ) ).
10:9:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. _E Fr ( a i^i x ) ).
11:10:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. A. b ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ).
12::	|- x e. _V
13:12,8:	|- ( a i^i x ) e. _V
14:13,11:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ).
15::	|- ( [. ( 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 ) = (/) ) )
16:14,15:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( ( 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 ) = (/) ) ).
17::	|- ( a i^i x ) C_ ( a i^i x )
18:2:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. -. ( a i^i x ) = (/) ).
19:18:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( a i^i x ) =/= (/) ).
20:17,19:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) ).
qed:16,20:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( 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 C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ).

Theorem

simplbi2comtVD 37325

Virtual deduction proof of simplbi2comt 636. 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. simplbi2comt 636 is simplbi2comtVD 37325 without virtual deductions and was automatically derived from simplbi2comtVD 37325.

1::	|- (. ( ph <-> ( ps /\ ch ) ) ->. ( ph <-> ( ps /\ ch ) ) ).
2:1:	|- (. ( ph <-> ( ps /\ ch ) ) ->. ( ( ps /\ ch ) -> ph ) ).
3:2:	|- (. ( ph <-> ( ps /\ ch ) ) ->. ( ps -> ( ch -> ph ) ) ).
4:3:	|- (. ( ph <-> ( ps /\ ch ) ) ->. ( ch -> ( ps -> ph ) ) ).
qed:4:	|- ( ( ph <-> ( ps /\ ch ) ) -> ( ch -> ( ps -> ph ) ) )

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

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

Theorem

onfrALTlem2VD 37326*

Virtual deduction proof of onfrALTlem2 36956. 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. onfrALTlem2 36956 is onfrALTlem2VD 37326 without virtual deductions and was automatically derived from onfrALTlem2VD 37326.

1::	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ).
2:1:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( a i^i y ) ).
3:2:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. a ).
4::	|- (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
5::	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
6:5:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
7:4:	|- (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
8:6,7:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
9:8:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
10:9:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Tr x ).
11:1:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. y e. ( a i^i x ) ).
12:11:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. y e. x ).
13:2:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. y ).
14:10,12,13:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. x ).
15:3,14:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( a i^i x ) ).
16:13,15:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( ( a i^i x ) i^i y ) ).
17:16:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ).
18:17:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. A. z ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ).
19:18:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( a i^i y ) C_ ( ( a i^i x ) i^i y ) ).
20::	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ).
21:20:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( ( a i^i x ) i^i y ) = (/) ).
22:19,21:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( a i^i y ) = (/) ).
23:20:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. y e. ( a i^i x ) ).
24:23:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. y e. a ).
25:22,24:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( y e. a /\ ( a i^i y ) = (/) ) ).
26:25:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) ).
27:26:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. A. y ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) ).
28:27:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) ).
29::	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ).
30:29:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ).
31:28,30:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y ( y e. a /\ ( a i^i y ) = (/) ) ).
qed:31:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).

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

|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).

Theorem

onfrALTlem1VD 37327*

Virtual deduction proof of onfrALTlem1 36958. 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. onfrALTlem1 36958 is onfrALTlem1VD 37327 without virtual deductions and was automatically derived from onfrALTlem1VD 37327.

1::	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ ( a i^i x ) = (/) ) ->. ( x e. a /\ ( a i^i x ) = (/) ) ).
2:1:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ ( a i^i x ) = (/) ) ->. E. x ( x e. a /\ ( a i^i x ) = (/) ) ).
3:2:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ ( a i^i x ) = (/) ) ->. E. y [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) ).
4::	|- ( [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )
5:4:	|- A. y ( [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )
6:5:	|- ( E. y [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) <-> E. y ( y e. a /\ ( a i^i y ) = (/) ) )
7:3,6:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ ( a i^i x ) = (/) ) ->. E. y ( y e. a /\ ( a i^i y ) = (/) ) ).
8::	|- ( E. y e. a ( a i^i y ) = (/) <-> E. y ( y e. a /\ ( a i^i y ) = (/) ) )
qed:7,8:	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).

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

|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).

Theorem

onfrALTVD 37328

Virtual deduction proof of onfrALT 36959. 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. onfrALT 36959 is onfrALTVD 37328 without virtual deductions and was automatically derived from onfrALTVD 37328.

1::	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).
2::	|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).
3:1:	|- (. ( a C_ On /\ a =/= (/) ) ,. x e. a ->. ( -. ( a i^i x ) = (/) -> E. y e. a ( a i^i y ) = (/) ) ).
4:2:	|- (. ( a C_ On /\ a =/= (/) ) ,. x e. a ->. ( ( a i^i x ) = (/) -> E. y e. a ( a i^i y ) = (/) ) ).
5::	|- ( ( a i^i x ) = (/) \/ -. ( a i^i x ) = (/) )
6:5,4,3:	|- (. ( a C_ On /\ a =/= (/) ) ,. x e. a ->. E. y e. a ( a i^i y ) = (/) ).
7:6:	|- (. ( a C_ On /\ a =/= (/) ) ->. ( x e. a -> E. y e. a ( a i^i y ) = (/) ) ).
8:7:	|- (. ( a C_ On /\ a =/= (/) ) ->. A. x ( x e. a -> E. y e. a ( a i^i y ) = (/) ) ).
9:8:	|- (. ( a C_ On /\ a =/= (/) ) ->. ( E. x x e. a -> E. y e. a ( a i^i y ) = (/) ) ).
10::	|- ( a =/= (/) <-> E. x x e. a )
11:9,10:	|- (. ( a C_ On /\ a =/= (/) ) ->. ( a =/= (/) -> E. y e. a ( a i^i y ) = (/) ) ).
12::	|- (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
13:12:	|- (. ( a C_ On /\ a =/= (/) ) ->. a =/= (/) ).
14:13,11:	|- (. ( a C_ On /\ a =/= (/) ) ->. E. y e. a ( a i^i y ) = (/) ).
15:14:	|- ( ( a C_ On /\ a =/= (/) ) -> E. y e. a ( a i^i y ) = (/) )
16:15:	|- A. a ( ( a C_ On /\ a =/= (/) ) -> E. y e. a ( a i^i y ) = (/) )
qed:16:	|- _E Fr On

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

|- _E Fr On

Theorem

csbeq2gVD 37329

Virtual deduction proof of csbeq2gOLD 36960. 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. csbeq2gOLD 36960 is csbeq2gVD 37329 without virtual deductions and was automatically derived from csbeq2gVD 37329.

1::	|- (. A e. V ->. A e. V ).
2:1:	|- (. A e. V ->. ( A. x B = C -> [. A / x ]. B = C ) ).
3:1:	|- (. A e. V ->. ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) ).
4:2,3:	|- (. A e. V ->. ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) ).
qed:4:	|- ( A e. V -> ( A. x B = C -> [_ A / x ]_ B = [_ A / x ]_ C ) )

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

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

Theorem

csbsngVD 37330

Virtual deduction proof of csbsng 4042. 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. csbsng 4042 is csbsngVD 37330 without virtual deductions and was automatically derived from csbsngVD 37330.

1::	|- (. A e. V ->. A e. V ).
2:1:	|- (. A e. V ->. ( [. A / x ]. y = B <-> [_ A / x ]_ y = [_ A / x ]_ B ) ).
3:1:	|- (. A e. V ->. [_ A / x ]_ y = y ).
4:3:	|- (. A e. V ->. ( [_ A / x ]_ y = [_ A / x ]_ B <-> y = [_ A / x ]_ B ) ).
5:2,4:	|- (. A e. V ->. ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) ).
6:5:	|- (. A e. V ->. A. y ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) ).
7:6:	|- (. A e. V ->. { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } ).
8:1:	|- (. A e. V ->. { y | [. A / x ]. y = B } = [_ A / x ]_ { y | y = B } ).
9:7,8:	|- (. A e. V ->. [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } ).
10::	|- { B } = { y | y = B }
11:10:	|- A. x { B } = { y | y = B }
12:1,11:	|- (. A e. V ->. [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B } ).
13:9,12:	|- (. A e. V ->. [_ A / x ]_ { B } = { y | y = [_ A / x ]_ B } ).
14::	|- { [_ A / x ]_ B } = { y | y = [_ A / x ]_ B }
15:13,14:	|- (. A e. V ->. [_ A / x ]_ { B } = { [_ A / x ]_ B } ).
qed:15:	|- ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )

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

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

Theorem

csbxpgVD 37331

Virtual deduction proof of csbxpgOLD 37254. 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. csbxpgOLD 37254 is csbxpgVD 37331 without virtual deductions and was automatically derived from csbxpgVD 37331.

1::	|- (. A e. V ->. A e. V ).
2:1:	|- (. A e. V ->. ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) ).
3:1:	|- (. A e. V ->. [_ A / x ]_ w = w ).
4:3:	|- (. A e. V ->. ( [_ A / x ]_ w e. [_ A / x ]_ B <-> w e. [_ A / x ]_ B ) ).
5:2,4:	|- (. A e. V ->. ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) ).
6:1:	|- (. A e. V ->. ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) ).
7:1:	|- (. A e. V ->. [_ A / x ]_ y = y ).
8:7:	|- (. A e. V ->. ( [_ A / x ]_ y e. [_ A / x ]_ C <-> y e. [_ A / x ]_ C ) ).
9:6,8:	|- (. A e. V ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
10:5,9:	|- (. A e. V ->. ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ).
11:1:	|- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) ).
12:10,11:	|- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ).
13:1:	|- (. A e. V ->. ( [. A / x ]. z = <. w ,. y >. <-> z = <. w , y >. ) ).
14:12,13:	|- (. A e. V ->. ( ( [. A / x ]. z = <. w ,. y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
15:1:	|- (. A e. V ->. ( [. A / x ]. ( z = <. w ,. y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) ).
16:14,15:	|- (. A e. V ->. ( [. A / x ]. ( z = <. w ,. y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
17:16:	|- (. A e. V ->. A. y ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
18:17:	|- (. A e. V ->. ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
19:1:	|- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ).
20:18,19:	|- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
21:20:	|- (. A e. V ->. A. w ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
22:21:	|- (. A e. V ->. ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
23:1:	|- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ).
24:22,23:	|- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
25:24:	|- (. A e. V ->. A. z ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ).
26:25:	|- (. A e. V ->. { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
27:1:	|- (. A e. V ->. [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ).
28:26,27:	|- (. A e. V ->. [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
29::	|- { <. w ,. y >. | ( w e. B /\ y e. C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
30::	|- ( B X. C ) = { <. w ,. y >. | ( w e. B /\ y e. C ) }
31:29,30:	|- ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
32:31:	|- A. x ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) }
33:1,32:	|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ).
34:28,33:	|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ).
35::	|- { <. w ,. y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
36::	|- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { <. w , y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) }
37:35,36:	|- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) }
38:34,37:	|- (. A e. V ->. [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) ).
qed:38:	|- ( A e. V -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )

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

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

Theorem

csbresgVD 37332

Virtual deduction proof of csbresgOLD 37256. 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. csbresgOLD 37256 is csbresgVD 37332 without virtual deductions and was automatically derived from csbresgVD 37332.

1::	|- (. A e. V ->. A e. V ).
2:1:	|- (. A e. V ->. [_ A / x ]_ _V = _V ).
3:2:	|- (. A e. V ->. ( [_ A / x ]_ C X. [_ A / x ]_ _V ) = ( [_ A / x ]_ C X. _V ) ).
4:1:	|- (. A e. V ->. [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. [_ A / x ]_ _V ) ).
5:3,4:	|- (. A e. V ->. [_ A / x ]_ ( C X. _V ) = ( [_ A / x ]_ C X. _V ) ).
6:5:	|- (. A e. V ->. ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) ) ).
7:1:	|- (. A e. V ->. [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X. _V ) ) ).
8:6,7:	|- (. A e. V ->. [_ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) ) ).
9::	|- ( B |` C ) = ( B i^i ( C X. _V ) )
10:9:	|- A. x ( B |` C ) = ( B i^i ( C X. _V ) )
11:1,10:	|- (. A e. V ->. [_ A / x ]_ ( B |` C ) = [_ A / x ]_ ( B i^i ( C X. _V ) ) ).
12:8,11:	|- (. A e. V ->. [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B i^i ( [_