Theorem vtocl2 3162

Description: Implicit substitution of classes for setvar variables. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Hypotheses

Ref	Expression
vtocl2.1
vtocl2.2
vtocl2.3
vtocl2.4

Assertion

Ref	Expression
vtocl2

Distinct variable groups:   ,,   ,,   ,,

Proof of Theorem vtocl2

Step	Hyp	Ref	Expression
1		vtocl2.1	. . . . . 6
2	1	isseti 3115	. . . . 5
3		vtocl2.2	. . . . . 6
4	3	isseti 3115	. . . . 5
5		eeanv 1988	. . . . . 6
6		vtocl2.3	. . . . . . . 8
7	6	biimpd 207	. . . . . . 7
8	7	2eximi 1657	. . . . . 6
9	5, 8	sylbir 213	. . . . 5
10	2, 4, 9	mp2an 672	. . . 4
11		19.36v 1762	. . . . 5
12	11	exbii 1667	. . . 4
13	10, 12	mpbi 208	. . 3
14	13	19.36iv 1763	. 2
15		vtocl2.4	. . 3
16	15	ax-gen 1618	. 2
17	14, 16	mpg 1620	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  cvv 3109

This theorem is referenced by:  caovord  6486  sornom  8678  wloglei  10110  ipodrsima  15795  mpfind  18205  mclsppslem  28943  monotoddzzfi  30878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111