MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtocl2g Unicode version

Theorem vtocl2g 3171
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)
Hypotheses
Ref Expression
vtocl2g.1
vtocl2g.2
vtocl2g.3
Assertion
Ref Expression
vtocl2g
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem vtocl2g
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . 2
3 nfcv 2619 . 2
4 nfv 1707 . 2
5 nfv 1707 . 2
6 vtocl2g.1 . 2
7 vtocl2g.2 . 2
8 vtocl2g.3 . 2
91, 2, 3, 4, 5, 6, 7, 8vtocl2gf 3169 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818
This theorem is referenced by:  vtocl4g  3178  ifexg  4011  uniprg  4263  intprg  4321  opthg  4727  opelopabsb  4762  vtoclr  5049  elimasng  5368  cnvsng  5499  funopg  5625  f1osng  5859  fsng  6070  fvsng  6105  unexb  6600  op1stg  6812  op2ndg  6813  xpsneng  7622  xpcomeng  7629  sbth  7657  unxpdom  7747  fpwwe2lem5  9033  prcdnq  9392  mhmlem  16190  2pthoncl  24605  brimageg  29577  brdomaing  29585  brrangeg  29586  rankung  29823  mbfresfi  30061  zindbi  30882  2sbc6g  31322  2sbc5g  31323  fmulcl  31575
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-13 1999  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-nfc 2607  df-v 3111
  Copyright terms: Public domain W3C validator