P. 342 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

trintALT 34101*

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

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

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 34103

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

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 34104

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

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

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

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

Virtual deduction proof of onfrALTlem4 33728. 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 33728 is onfrALTlem4VD 34106 without virtual deductions and was automatically derived from onfrALTlem4VD 34106.

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

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

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 34108

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

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

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

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

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

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 34111

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

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 34112

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

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 34113

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

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 34114

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

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 34115

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

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 ( [_ A / x ]_ C X. _V ) ) ).
13::	|- ( [_ A / x ]_ B |` [_ A / x ]_ C ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X. _V ) )
14:12,13:	|- (. A e. V ->. [_ A / x ]_ ( B |` C ) = ( [_ A / x ]_ B |` [_ A / x ]_ C ) ).
qed:14:	|- ( 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

csbrngVD 34116

Virtual deduction proof of csbrngOLD 34040. 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. csbrngOLD 34040 is csbrngVD 34116 without virtual deductions and was automatically derived from csbrngVD 34116.

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

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

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

Theorem

csbima12gALTVD 34117

Virtual deduction proof of csbima12gALTOLD 34041. 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. csbima12gALTOLD 34041 is csbima12gALTVD 34117 without virtual deductions and was automatically derived from csbima12gALTVD 34117.

1::	|- (. A e. C ->. A e. C ).
2:1:	|- (. A e. C ->. [_ A / x ]_ ( F |` B ) = ( [_ A / x ]_ F |` [_ A / x ]_ B ) ).
3:2:	|- (. A e. C ->. ran [_ A / x ]_ ( F |` B ) = ran ( [_ A / x ]_ F |` [_ A / x ]_ B ) ).
4:1:	|- (. A e. C ->. [_ A / x ]_ ran ( F |` B ) = ran [_ A / x ]_ ( F |` B ) ).
5:3,4:	|- (. A e. C ->. [_ A / x ]_ ran ( F |` B ) = ran ( [_ A / x ]_ F |` [_ A / x ]_ B ) ).
6::	|- ( F " B ) = ran ( F |` B )
7:6:	|- A. x ( F " B ) = ran ( F |` B )
8:1,7:	|- (. A e. C ->. [_ A / x ]_ ( F " B ) = [_ A / x ]_ ran ( F |` B ) ).
9:5,8:	|- (. A e. C ->. [_ A / x ]_ ( F " B ) = ran ( [_ A / x ]_ F |` [_ A / x ]_ B ) ).
10::	|- ( [_ A / x ]_ F " [_ A / x ]_ B ) = ran ( [_ A / x ]_ F |` [_ A / x ]_ B )
11:9,10:	|- (. A e. C ->. [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) ).
qed:11:	|- ( A e. C -> [_ A / x ]_ ( F " B ) = ( [_ A / x ]_ F " [_ A / x ]_ B ) )

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

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

Theorem

csbunigVD 34118

Virtual deduction proof of csbunigOLD 34035. 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. csbunigOLD 34035 is csbunigVD 34118 without virtual deductions and was automatically derived from csbunigVD 34118.

1::	|- (. A e. V ->. A e. V ).
2:1:	|- (. A e. V ->. ( [. A / x ]. z e. y <-> z e. y ) ).
3:1:	|- (. A e. V ->. ( [. A / x ]. y e. B <-> y e. [_ A / x ]_ B ) ).
4:2,3:	|- (. A e. V ->. ( ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
5:1:	|- (. A e. V ->. ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( [. A / x ]. z e. y /\ [. A / x ]. y e. B ) ) ).
6:4,5:	|- (. A e. V ->. ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
7:6:	|- (. A e. V ->. A. y ( [. A / x ]. ( z e. y /\ y e. B ) <-> ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
8:7:	|- (. A e. V ->. ( E. y [. A / x ]. ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
9:1:	|- (. A e. V ->. ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y [. A / x ]. ( z e. y /\ y e. B ) ) ).
10:8,9:	|- (. A e. V ->. ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
11:10:	|- (. A e. V ->. A. z ( [. A / x ]. E. y ( z e. y /\ y e. B ) <-> E. y ( z e. y /\ y e. [_ A / x ]_ B ) ) ).
12:11:	|- (. A e. V ->. { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ).
13:1:	|- (. A e. V ->. [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | [. A / x ]. E. y ( z e. y /\ y e. B ) } ).
14:12,13:	|- (. A e. V ->. [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ).
15::	|- U. B = { z | E. y ( z e. y /\ y e. B ) }
16:15:	|- A. x U. B = { z | E. y ( z e. y /\ y e. B ) }
17:1,16:	|- (. A e. V ->. [. A / x ]. U. B = { z | E. y ( z e. y /\ y e. B ) } ).
18:1,17:	|- (. A e. V ->. [_ A / x ]_ U. B = [_ A / x ]_ { z | E. y ( z e. y /\ y e. B ) } ).
19:14,18:	|- (. A e. V ->. [_ A / x ]_ U. B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) } ).
20::	|- U. [_ A / x ]_ B = { z | E. y ( z e. y /\ y e. [_ A / x ]_ B ) }
21:19,20:	|- (. A e. V ->. [_ A / x ]_ U. B = U. [_ A / x ]_ B ).
qed:21:	|- ( A e. V -> [_ A / x ]_ U. B = U. [_ A / x ]_ B )

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

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

Theorem

csbfv12gALTVD 34119

Virtual deduction proof of csbfv12gALTOLD 34036. 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. csbfv12gALTOLD 34036 is csbfv12gALTVD 34119 without virtual deductions and was automatically derived from csbfv12gALTVD 34119.

1::	|- (. A e. C ->. A e. C ).
2:1:	|- (. A e. C ->. [_ A / x ]_ { y } = { y } ).
3:1:	|- (. A e. C ->. [_ A / x ]_ ( F " { B } ) = ( [_ A / x ]_ F " [_ A / x ]_ { B } ) ).
4:1:	|- (. A e. C ->. [_ A / x ]_ { B } = { [_ A / x ]_ B } ).
5:4:	|- (. A e. C ->. ( [_ A / x ]_ F " [_ A / x ]_ { B } ) = ( [_ A / x ]_ F " { [_ A / x ]_ B } ) ).
6:3,5:	|- (. A e. C ->. [_ A / x ]_ ( F " { B } ) = ( [_ A / x ]_ F " { [_ A / x ]_ B } ) ).
7:1:	|- (. A e. C ->. ( [. A / x ]. ( F " { B } ) = { y } <-> [_ A / x ]_ ( F " { B } ) = [_ A / x ]_ { y } ) ).
8:6,2:	|- (. A e. C ->. ( [_ A / x ]_ ( F " { B } ) = [_ A / x ]_ { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
9:7,8:	|- (. A e. C ->. ( [. A / x ]. ( F " { B } ) = { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
10:9:	|- (. A e. C ->. A. y ( [. A / x ]. ( F " { B } ) = { y } <-> ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } ) ).
11:10:	|- (. A e. C ->. { y | [. A / x ]. ( F " { B } ) = { y } } = { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
12:1:	|- (. A e. C ->. [_ A / x ]_ { y | ( F " { B } ) = { y } } = { y | [. A / x ]. ( F " { B } ) = { y } } ).
13:11,12:	|- (. A e. C ->. [_ A / x ]_ { y | ( F " { B } ) = { y } } = { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
14:13:	|- (. A e. C ->. U. [_ A / x ]_ { y | ( F " { B } ) = { y } } = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
15:1:	|- (. A e. C ->. [_ A / x ]_ U. { y | ( F " { B } ) = { y } } = U. [_ A / x ]_ { y | ( F " { B } ) = { y } } ).
16:14,15:	|- (. A e. C ->. [_ A / x ]_ U. { y | ( F " { B } ) = { y } } = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
17::	|- ( F ` B ) = U. { y | ( F " { B } ) = { y } }
18:17:	|- A. x ( F ` B ) = U. { y | ( F " { B } ) = { y } }
19:1,18:	|- (. A e. C ->. [_ A / x ]_ ( F ` B ) = [_ A / x ]_ U. { y | ( F " { B } ) = { y } } ).
20:16,19:	|- (. A e. C ->. [_ A / x ]_ ( F ` B ) = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } } ).
21::	|- ( [_ A / x ]_ F ` [_ A / x ]_ B ) = U. { y | ( [_ A / x ]_ F " { [_ A / x ]_ B } ) = { y } }
22:20,21:	|- (. A e. C ->. [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) ).
qed:22:	|- ( A e. C -> [_ A / x ]_ ( F ` B ) = ( [_ A / x ]_ F ` [_ A / x ]_ B ) )

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

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

Theorem

con5VD 34120

Virtual deduction proof of con5 33698. 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. con5 33698 is con5VD 34120 without virtual deductions and was automatically derived from con5VD 34120.

1::	|- (. ( ph <-> -. ps ) ->. ( ph <-> -. ps ) ).
2:1:	|- (. ( ph <-> -. ps ) ->. ( -. ps -> ph ) ).
3:2:	|- (. ( ph <-> -. ps ) ->. ( -. ph -> -. -. ps ) ).
4::	|- ( ps <-> -. -. ps )
5:3,4:	|- (. ( ph <-> -. ps ) ->. ( -. ph -> ps ) ).
qed:5:	|- ( ( ph <-> -. ps ) -> ( -. ph -> ps ) )

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

|- ( ( ph <-> -. ps ) -> ( -. ph -> ps ) )

Theorem

relopabVD 34121

Virtual deduction proof of relopab 5117. 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. relopab 5117 is relopabVD 34121 without virtual deductions and was automatically derived from relopabVD 34121.

1::	|- (. y = v ->. y = v ).
2:1:	|- (. y = v ->. <. x ,. y >. = <. x ,. v >. ).
3::	|- (. y = v ,. x = u ->. x = u ).
4:3:	|- (. y = v ,. x = u ->. <. x ,. v >. = <. u , v >. ).
5:2,4:	|- (. y = v ,. x = u ->. <. x ,. y >. = <. u , v >. ).
6:5:	|- (. y = v ,. x = u ->. ( z = <. x ,. y >. -> z = <. u , v >. ) ).
7:6:	|- (. y = v ->. ( x = u -> ( z = <. x ,. y >. -> z = <. u , v >. ) ) ).
8:7:	|- ( y = v -> ( x = u -> ( z = <. x ,. y >. -> z = <. u , v >. ) ) )
9:8:	|- ( E. v y = v -> E. v ( x = u -> ( z = <. x , y >. -> z = <. u , v >. ) ) )
90::	|- ( v = y <-> y = v )
91:90:	|- ( E. v v = y <-> E. v y = v )
92::	|- E. v v = y
10:91,92:	|- E. v y = v
11:9,10:	|- E. v ( x = u -> ( z = <. x ,. y >. -> z = <. u , v >. ) )
12:11:	|- ( x = u -> E. v ( z = <. x ,. y >. -> z = <. u , v >. ) )
13::	|- ( E. v ( z = <. x ,. y >. -> z = <. u , v >. ) -> ( z = <. x , y >. -> E. v z = <. u , v >. ) )
14:12,13:	|- ( x = u -> ( z = <. x ,. y >. -> E. v z = <. u , v >. ) )
15:14:	|- ( E. u x = u -> E. u ( z = <. x ,. y >. -> E. v z = <. u , v >. ) )
150::	|- ( u = x <-> x = u )
151:150:	|- ( E. u u = x <-> E. u x = u )
152::	|- E. u u = x
16:151,152:	|- E. u x = u
17:15,16:	|- E. u ( z = <. x ,. y >. -> E. v z = <. u , v >. )
18:17:	|- ( z = <. x ,. y >. -> E. u E. v z = <. u , v >. )
19:18:	|- ( E. y z = <. x ,. y >. -> E. y E. u E. v z = <. u , v >. )
20::	|- ( E. y E. u E. v z = <. u ,. v >. -> E. u E. v z = <. u , v >. )
21:19,20:	|- ( E. y z = <. x ,. y >. -> E. u E. v z = <. u , v >. )
22:21:	|- ( E. x E. y z = <. x ,. y >. -> E. x E. u E. v z = <. u , v >. )
23::	|- ( E. x E. u E. v z = <. u ,. v >. -> E. u E. v z = <. u , v >. )
24:22,23:	|- ( E. x E. y z = <. x ,. y >. -> E. u E. v z = <. u , v >. )
25:24:	|- { z | E. x E. y z = <. x ,. y >. } C_ { z | E. u E. v z = <. u , v >. }
26::	|- x e. _V
27::	|- y e. _V
28:26,27:	|- ( x e. _V /\ y e. _V )
29:28:	|- ( z = <. x ,. y >. <-> ( z = <. x ,. y >. /\ ( x e. _V /\ y e. _V ) ) )
30:29:	|- ( E. y z = <. x ,. y >. <-> E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
31:30:	|- ( E. x E. y z = <. x ,. y >. <-> E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) )
32:31:	|- { z | E. x E. y z = <. x ,. y >. } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) }
320:25,32:	|- { z | E. x E. y ( z = <. x ,. y >. /\ ( x e. _V /\ y e. _V ) ) } C_ { z | E. u E. v z = <. u , v >. }
33::	|- u e. _V
34::	|- v e. _V
35:33,34:	|- ( u e. _V /\ v e. _V )
36:35:	|- ( z = <. u ,. v >. <-> ( z = <. u ,. v >. /\ ( u e. _V /\ v e. _V ) ) )
37:36:	|- ( E. v z = <. u ,. v >. <-> E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) )
38:37:	|- ( E. u E. v z = <. u ,. v >. <-> E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) )
39:38:	|- { z | E. u E. v z = <. u ,. v >. } = { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) }
40:320,39:	|- { z | E. x E. y ( z = <. x ,. y >. /\ ( x e. _V /\ y e. _V ) ) } C_ { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) }
41::	|- { <. x ,. y >. | ( x e. _V /\ y e. _V ) } = { z | E. x E. y ( z = <. x , y >. /\ ( x e. _V /\ y e. _V ) ) }
42::	|- { <. u ,. v >. | ( u e. _V /\ v e. _V ) } = { z | E. u E. v ( z = <. u , v >. /\ ( u e. _V /\ v e. _V ) ) }
43:40,41,42:	|- { <. x ,. y >. | ( x e. _V /\ y e. _V ) } C_ { <. u , v >. | ( u e. _V /\ v e. _V ) }
44::	|- { <. u ,. v >. | ( u e. _V /\ v e. _V ) } = ( _V X. _V )
45:43,44:	|- { <. x ,. y >. | ( x e. _V /\ y e. _V ) } C_ ( _V X. _V )
46:28:	|- ( ph -> ( x e. _V /\ y e. _V ) )
47:46:	|- { <. x ,. y >. | ph } C_ { <. x ,. y >. | ( x e. _V /\ y e. _V ) }
48:45,47:	|- { <. x ,. y >. | ph } C_ ( _V X. _V )
qed:48:	|- Rel { <. x ,. y >. | ph }

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

|- Rel { <. x , y >. | ph }

Theorem

19.41rgVD 34122

Virtual deduction proof of 19.41rg 33736. 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. 19.41rg 33736 is 19.41rgVD 34122 without virtual deductions and was automatically derived from 19.41rgVD 34122. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	|- ( ps -> ( ph -> ( ph /\ ps ) ) )
2:1:	|- ( ( ps -> A. x ps ) -> ( ps -> ( ph -> ( ph /\ ps ) ) ) )
3:2:	|- A. x ( ( ps -> A. x ps ) -> ( ps -> ( ph -> ( ph /\ ps ) ) ) )
4:3:	|- ( A. x ( ps -> A. x ps ) -> ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) )
5::	|- (. A. x ( ps -> A. x ps ) ->. A. x ( ps -> A. x ps ) ).
6:4,5:	|- (. A. x ( ps -> A. x ps ) ->. ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) ).
7::	|- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. A. x ps ).
8:6,7:	|- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. A. x ( ph -> ( ph /\ ps ) ) ).
9:8:	|- (. A. x ( ps -> A. x ps ) ,. A. x ps ->. ( E. x ph -> E. x ( ph /\ ps ) ) ).
10:9:	|- (. A. x ( ps -> A. x ps ) ->. ( A. x ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) ).
11:5:	|- (. A. x ( ps -> A. x ps ) ->. ( ps -> A. x ps ) ).
12:10,11:	|- (. A. x ( ps -> A. x ps ) ->. ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) ).
13:12:	|- (. A. x ( ps -> A. x ps ) ->. ( E. x ph -> ( ps -> E. x ( ph /\ ps ) ) ) ).
14:13:	|- (. A. x ( ps -> A. x ps ) ->. ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) ).
qed:14:	|- ( A. x ( ps -> A. x ps ) -> ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) )

|- ( A. x ( ps -> A. x ps ) -> ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) )

Theorem

2pm13.193VD 34123

Virtual deduction proof of 2pm13.193 33738. 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. 2pm13.193 33738 is 2pm13.193VD 34123 without virtual deductions and was automatically derived from 2pm13.193VD 34123. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ).
2:1:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( x = u /\ y = v ) ).
3:2:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. x = u ).
4:1:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. [ u / x ] [ v / y ] ph ).
5:3,4:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ u / x ] [ v / y ] ph /\ x = u ) ).
6:5:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ v / y ] ph /\ x = u ) ).
7:6:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. [ v / y ] ph ).
8:2:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. y = v ).
9:7,8:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( [ v / y ] ph /\ y = v ) ).
10:9:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ph /\ y = v ) ).
11:10:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ph ).
12:2,11:	|- (. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
13:12:	|- ( ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) -> ( ( x = u /\ y = v ) /\ ph ) )
14::	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
15:14:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( x = u /\ y = v ) ).
16:15:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. y = v ).
17:14:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. ph ).
18:16,17:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ph /\ y = v ) ).
19:18:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ v / y ] ph /\ y = v ) ).
20:15:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. x = u ).
21:19:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. [ v / y ] ph ).
22:20,21:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ v / y ] ph /\ x = u ) ).
23:22:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( [ u / x ] [ v / y ] ph /\ x = u ) ).
24:23:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. [ u / x ] [ v / y ] ph ).
25:15,24:	|- (. ( ( x = u /\ y = v ) /\ ph ) ->. ( ( x = u /\ y = v ) /\ [ u / x ] [ v / y ] ph ) ).
26:25:	|- ( ( ( x = u /\ y =