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

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

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-26249)
  Hilbert Space Explorer  Hilbert Space Explorer
(26250-27773)
  Users' Mathboxes  Users' Mathboxes
(27774-38860)
 

Theorem List for Metamath Proof Explorer - 36701-36800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
TheoremsucidALTVD 36701 A set belongs to its successor. Alternate proof of sucid 5489. 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 36702 is sucidALTVD 36701 without virtual deductions and was automatically derived from sucidALTVD 36701. 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 5416, 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 8070.
h1::  |-  A  e.  _V
2:1:  |-  A  e.  { A }
3:2:  |-  A  e.  ( { A }  u.  A )
4::  |-  suc  A  =  ( { A }  u.  A )
qed:3,4:  |-  A  e.  suc  A
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  A  e.  suc  A
 
TheoremsucidALT 36702 A set belongs to its successor. This proof was automatically derived from sucidALTVD 36701 using translatewithout_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  A  e.  suc  A
 
TheoremsucidVD 36703 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 5489 is sucidVD 36703 without virtual deductions and was automatically derived from sucidVD 36703.
h1::  |-  A  e.  _V
2:1:  |-  A  e.  { A }
3:2:  |-  A  e.  ( A  u.  { A } )
4::  |-  suc  A  =  ( A  u.  { A } )
qed:3,4:  |-  A  e.  suc  A
(Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  A  e.  _V   =>    |-  A  e.  suc  A
 
Theoremimbi12VD 36704 Implication form of imbi12i 324. 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 320 is imbi12VD 36704 without virtual deductions and was automatically derived from imbi12VD 36704.
1::  |-  (. ( ph  <->  ps )  ->.  ( ph  <->  ps ) ).
2::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ch  <->  th ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ph  ->  ch ) ).
4:1,3:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  ch ) ).
5:2,4:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  th ) ).
6:5:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ph  ->  ch )  ->  ( ps  ->  th ) ) ).
7::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ps  ->  th ) ).
8:1,7:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  th ) ).
9:2,8:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  ch ) ).
10:9:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ps  ->  th )  ->  ( ph  ->  ch ) ) ).
11:6,10:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ).
12:11:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) ).
qed:12:  |-  ( ( ph  <->  ps )  ->  ( ( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  <->  ps )  ->  (
 ( ch  <->  th )  ->  (
 ( ph  ->  ch )  <->  ( ps  ->  th )
 ) ) )
 
Theoremimbi13VD 36705 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 36307 is imbi13VD 36705 without virtual deductions and was automatically derived from imbi13VD 36705.
1::  |-  (. ( ph  <->  ps )  ->.  ( ph  <->  ps ) ).
2::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ch  <->  th ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ta  <->  et ) ).
4:2,3:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ( ch  ->  ta )  <->  ( th  ->  et ) ) ).
5:1,4:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ).
6:5:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ).
7:6:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ) ).
qed:7:  |-  ( ( ph  <->  ps )  ->  ( ( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  (
 ( ph  <->  ps )  ->  (
 ( ch  <->  th )  ->  (
 ( ta  <->  et )  ->  (
 ( ph  ->  ( ch 
 ->  ta ) )  <->  ( ps  ->  ( th  ->  et )
 ) ) ) ) )
 
Theoremsbcim2gVD 36706 Distribution of class substitution over a left-nested implication. Similar to sbcimg 3319. 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 36329 is sbcim2gVD 36706 without virtual deductions and was automatically derived from sbcim2gVD 36706.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2::  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ).
3:1,2:  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ).
4:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ps  ->  ch )  <->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
5:3,4:  |-  (. A  e.  B ,. [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->.  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
6:5:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  ->  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) ).
7::  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ).
8:4,7:  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ).
9:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ( ps  ->  ch ) ) ) ).
10:8,9:  |-  (. A  e.  B ,. ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->.  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ).
11:10:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) )  ->  [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) ) ) ).
12:6,11:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) ).
qed:12:  |-  ( A  e.  B  ->  ( [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  ( [. A  /  x ]. ps  ->  [. A  /  x ]. ch ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 [. A  /  x ]. ( ph  ->  ( ps  ->  ch ) )  <->  ( [. A  /  x ]. ph  ->  (
 [. A  /  x ].
 ps  ->  [. A  /  x ].
 ch ) ) ) )
 
TheoremsbcbiVD 36707 Implication form of sbcbiiOLD 36322. 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 36330 is sbcbiVD 36707 without virtual deductions and was automatically derived from sbcbiVD 36707.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2::  |-  (. A  e.  B ,. A. x ( ph  <->  ps )  ->.  A. x ( ph  <->  ps ) ).
3:1,2:  |-  (. A  e.  B ,. A. x ( ph  <->  ps )  ->.  [. A  /  x ]. ( ph  <->  ps ) ).
4:1,3:  |-  (. A  e.  B ,. A. x ( ph  <->  ps )  ->.  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ).
5:4:  |-  (. A  e.  B  ->.  ( A. x ( ph  <->  ps )  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ) ).
qed:5:  |-  ( A  e.  B  ->  ( A. x ( ph  <->  ps )  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ]. ps ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 A. x ( ph  <->  ps )  ->  ( [. A  /  x ]. ph  <->  [. A  /  x ].
 ps ) ) )
 
TheoremtrsbcVD 36708* 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 36331 is trsbcVD 36708 without virtual deductions and was automatically derived from trsbcVD 36708.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  y  <->  z  e.  y ) ).
3:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  x  <->  y  e.  A ) ).
4:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. z  e.  x  <->  z  e.  A ) ).
5:1,2,3,4:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ).
6:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( [. A  /  x ]. z  e.  y  ->  ( [. A  /  x ]. y  e.  x  ->  [. A  /  x ]. z  e.  x ) ) ) ).
7:5,6:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) ) ) ).
8::  |-  ( ( z  e.  y  ->  ( y  e.  A  ->  z  e.  A ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
9:7,8:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
10::  |-  ( ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
11:10:  |-  A. x ( ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
12:1,11:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( z  e.  y  ->  ( y  e.  x  ->  z  e.  x ) )  <->  [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
13:9,12:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
14:13:  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
15:14:  |-  (. A  e.  B  ->.  ( A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
16:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y [. A  /  x ]. ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
17:15,16:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
18:17:  |-  (. A  e.  B  ->.  A. z ( [. A  /  x ]. A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
19:18:  |-  (. A  e.  B  ->.  ( A. z [. A  /  x ]. A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
20:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z [. A  /  x ]. A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
21:19,20:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) ) ).
22::  |-  ( Tr  A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  A )  ->  z  e.  A ) )
23:21,22:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. z A. y ( (  z  e.  y  /\  y  e.  x )  ->  z  e.  x )  <->  Tr  A ) ).
24::  |-  ( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
25:24:  |-  A. x ( Tr  x  <->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
26:1,25:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  [. A  /  x ]. A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) ).
27:23,26:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. Tr  x  <->  Tr  A ) ).
qed:27:  |-  ( A  e.  B  ->  ( [. A  /  x ]. Tr  x  <->  Tr  A ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 [. A  /  x ].
 Tr  x  <->  Tr  A ) )
 
TheoremtruniALTVD 36709* 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 36332 is truniALTVD 36709 without virtual deductions and was automatically derived from truniALTVD 36709.
1::  |-  (. A. x  e.  A Tr  x  ->.  A. x  e.  A  Tr  x ).
2::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  ( z  e.  y  /\  y  e.  U. A ) ).
3:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  z  e.  y ).
4:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  y  e.  U. A ).
5:4:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  E. q ( y  e.  q  /\  q  e.  A ) ).
6::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  ( y  e.  q  /\  q  e.  A ) ).
7:6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  y  e.  q ).
8:6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  q  e.  A ).
9:1,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  [ q  /  x ] Tr  x ).
10:8,9:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  Tr  q ).
11:3,7,10:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  z  e.  q ).
12:11,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  z  e.  U. A ).
13:12:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ).
14:13:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  A. q ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ).
15:14:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  ( E. q ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ).
16:5,15:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  z  e.  U. A ).
17:16:  |-  (. A. x  e.  A Tr  x  ->.  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A ) ).
18:17:  |-  (. A. x  e.  A Tr  x  ->.  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A ) ).
19:18:  |-  (. A. x  e.  A Tr  x  ->.  Tr  U. A ).
qed:19:  |-  ( A. x  e.  A Tr  x  ->  Tr  U. A )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
 
Theoremee33VD 36710 Non-virtual deduction form of e33 36555. 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 36308 is ee33VD 36710 without virtual deductions and was automatically derived from ee33VD 36710.
h1::  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
h2::  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
h3::  |-  ( th  ->  ( ta  ->  et ) )
4:1,3:  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  ->  et ) ) ) )
5:4:  |-  ( ta  ->  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) ) )
6:2,5:  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) ) ) ) )
7:6:  |-  ( ps  ->  ( ch  ->  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) ) ) )
8:7:  |-  ( ch  ->  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) ) )
qed:8:  |-  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( ph  ->  ( ps  ->  ( ch  ->  th )
 ) )   &    |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )   &    |-  ( th  ->  ( ta  ->  et ) )   =>    |-  ( ph  ->  ( ps  ->  ( ch  ->  et ) ) )
 
TheoremtrintALTVD 36711* The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 36712. 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 36712 is trintALTVD 36711 without virtual deductions and was automatically derived from trintALTVD 36711.
1::  |-  (. A. x  e.  A Tr  x  ->.  A. x  e.  A Tr  x ).
2::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( z  e.  y  /\  y  e.  |^| A ) ).
3:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  z  e.  y ).
4:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  y  e.  |^| A ).
5:4:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q  e.  A y  e.  q ).
6:5:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( q  e.  A  ->  y  e.  q ) ).
7::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  q  e.  A ).
8:7,6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  y  e.  q ).
9:7,1:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  [ q  /  x ] Tr  x ).
10:7,9:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  Tr  q ).
11:10,3,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  z  e.  q ).
12:11:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( q  e.  A  ->  z  e.  q ) ).
13:12:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q ( q  e.  A  ->  z  e.  q ) ).
14:13:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q  e.  A z  e.  q ).
15:3,14:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  z  e.  |^| A ).
16:15:  |-  (. A. x  e.  A Tr  x  ->.  ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  |^| A ) ).
17:16:  |-  (. A. x  e.  A Tr  x  ->.  A. z A. y ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  |^| A ) ).
18:17:  |-  (. A. x  e.  A Tr  x  ->.  Tr  |^| A ).
qed:18:  |-  ( A. x  e.  A Tr  x  ->  Tr  |^| A )
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
 
TheoremtrintALT 36712* The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 36712 is an alternative proof of trint 4504. trintALT 36712 is trintALTVD 36711 without virtual deductions and was automatically derived from trintALTVD 36711 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
 
Theoremundif3VD 36713 The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3711. 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 3711 is undif3VD 36713 without virtual deductions and was automatically derived from undif3VD 36713.
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 ) )
 
TheoremsbcssgVD 36714 Virtual deduction proof of sbcssg 3884. 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 3884 is sbcssgVD 36714 without virtual deductions and was automatically derived from sbcssgVD 36714.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) ).
3:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) ).
4:2,3:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. y  e.  C  ->  [. A  /  x ]. y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D  ) ) ).
5:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  ( [. A  /  x ]. y  e.  C  ->  [. A  /  x ]. y  e.  D ) ) ).
6:4,5:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D ) ) ).
7:6:  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D ) ) ).
8:7:  |-  (. A  e.  B  ->.  ( A. y [. A  /  x ]. ( y  e.  C  ->  y  e.  D )  <->  A. y ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D )  ) ).
9:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( y  e.  C  ->  y  e.  D )  <->  A. y [. A  /  x ]. ( y  e.  C  ->  y  e.  D ) ) ).
10:8,9:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. A. y ( y  e.  C  ->  y  e.  D )  <->  A. y ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D )  ) ).
11::  |-  ( C  C_  D  <->  A. y ( y  e.  C  ->  y  e.  D ) )
110:11:  |-  A. x ( C  C_  D  <->  A. y ( y  e.  C  ->  y  e.  D ) )
12:1,110:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. C  C_  D  <->  [. A  /  x ]. A. y ( y  e.  C  ->  y  e.  D ) ) ).
13:10,12:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. C  C_  D  <->  A. y ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D ) ) ).
14::  |-  ( [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D  <->  A.  y ( y  e.  [_ A  /  x ]_ C  ->  y  e.  [_ A  /  x ]_ D ) )
15:13,14:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. C  C_  D  <->  [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D ) ).
qed:15:  |-  ( A  e.  B  ->  ( [. A  /  x ]. C  C_  D  <->  [_  A  /  x ]_ C  C_  [_ A  /  x ]_ D ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  (
 [. A  /  x ]. C  C_  D  <->  [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D ) )
 
TheoremcsbingVD 36715 Virtual deduction proof of csbingOLD 36649. 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 36649 is csbingVD 36715 without virtual deductions and was automatically derived from csbingVD 36715.
1::  |-  (. A  e.  B  ->.  A  e.  B ).
2::  |-  ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D )  }
20:2:  |-  A. x ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) }
30:1,20:  |-  (. A  e.  B  ->.  [. A  /  x ]. ( C  i^i  D )  =  { y  |  ( y  e.  C  /\  y  e.  D ) } ).
3:1,30:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) } ).
4:1:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ { y  |  ( y  e.  C  /\  y  e.  D ) }  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
5:3,4:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) } ).
6:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  C  <->  y  e.  [_ A  /  x ]_ C ) ).
7:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. y  e.  D  <->  y  e.  [_ A  /  x ]_ D ) ).
8:6,7:  |-  (. A  e.  B  ->.  ( ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D )  ) ).
9:1:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( [. A  /  x ]. y  e.  C  /\  [. A  /  x ]. y  e.  D ) ) ).
10:9,8:  |-  (. A  e.  B  ->.  ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
11:10:  |-  (. A  e.  B  ->.  A. y ( [. A  /  x ]. ( y  e.  C  /\  y  e.  D )  <->  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) ) ).
12:11:  |-  (. A  e.  B  ->.  { y  |  [. A  /  x ]. ( y  e.  C  /\  y  e.  D ) }  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
13:5,12:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  { y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) } ).
14::  |-  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D )  =  {  y  |  ( y  e.  [_ A  /  x ]_ C  /\  y  e.  [_ A  /  x ]_ D ) }
15:13,14:  |-  (. A  e.  B  ->.  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) ).
qed:15:  |-  ( A  e.  B  ->  [_ A  /  x ]_ ( C  i^i  D )  =  (  [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( A  e.  B  ->  [_ A  /  x ]_ ( C  i^i  D )  =  ( [_ A  /  x ]_ C  i^i  [_ A  /  x ]_ D ) )
 
TheoremonfrALTlem5VD 36716* Virtual deduction proof of onfrALTlem5 36338. 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 36338 is onfrALTlem5VD 36716 without virtual deductions and was automatically derived from onfrALTlem5VD 36716.
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 )  =  (/) ) )
 
TheoremonfrALTlem4VD 36717* Virtual deduction proof of onfrALTlem4 36339. 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 36339 is onfrALTlem4VD 36717 without virtual deductions and was automatically derived from onfrALTlem4VD 36717.
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 )  =  (/) ) )
 
TheoremonfrALTlem3VD 36718* Virtual deduction proof of onfrALTlem3 36340. 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 36340 is onfrALTlem3VD 36718 without virtual deductions and was automatically derived from onfrALTlem3VD 36718.
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 )  =  (/) ).
 
Theoremsimplbi2comtVD 36719 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 36719 without virtual deductions and was automatically derived from simplbi2comtVD 36719.
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 ) ) )
 
TheoremonfrALTlem2VD 36720* Virtual deduction proof of onfrALTlem2 36342. 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 36342 is onfrALTlem2VD 36720 without virtual deductions and was automatically derived from onfrALTlem2VD 36720.
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 )  =  (/) ).
 
TheoremonfrALTlem1VD 36721* Virtual deduction proof of onfrALTlem1 36344. 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 36344 is onfrALTlem1VD 36721 without virtual deductions and was automatically derived from onfrALTlem1VD 36721.
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 )  =  (/) ).
 
TheoremonfrALTVD 36722 Virtual deduction proof of onfrALT 36345. 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 36345 is onfrALTVD 36722 without virtual deductions and was automatically derived from onfrALTVD 36722.
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
 
Theoremcsbeq2gVD 36723 Virtual deduction proof of csbeq2gOLD 36346. 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 36346 is csbeq2gVD 36723 without virtual deductions and was automatically derived from csbeq2gVD 36723.
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 ) )
 
TheoremcsbsngVD 36724 Virtual deduction proof of csbsng 4030. 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 4030 is csbsngVD 36724 without virtual deductions and was automatically derived from csbsngVD 36724.
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 } )
 
TheoremcsbxpgVD 36725 Virtual deduction proof of csbxpgOLD 36648. 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 36648 is csbxpgVD 36725 without virtual deductions and was automatically derived from csbxpgVD 36725.
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 ) )
 
TheoremcsbresgVD 36726 Virtual deduction proof of csbresgOLD 36650. 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 36650 is csbresgVD 36726 without virtual deductions and was automatically derived from csbresgVD 36726.
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 ) )
 
TheoremcsbrngVD 36727 Virtual deduction proof of csbrngOLD 36651. 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 36651 is csbrngVD 36727 without virtual deductions and was automatically derived from csbrngVD 36727.
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 )
 
Theoremcsbima12gALTVD 36728 Virtual deduction proof of csbima12gALTOLD 36652. 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 36652 is csbima12gALTVD 36728 without virtual deductions and was automatically derived from csbima12gALTVD 36728.
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 ) )
 
TheoremcsbunigVD 36729 Virtual deduction proof of csbunigOLD 36646. 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 36646 is csbunigVD 36729 without virtual deductions and was automatically derived from csbunigVD 36729.
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 )