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

Theorem vtoclga 3159
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
Hypotheses
Ref Expression
vtoclga.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtoclga.2  |-  ( x  e.  B  ->  ph )
Assertion
Ref Expression
vtoclga  |-  ( A  e.  B  ->  ps )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem vtoclga
StepHypRef Expression
1 nfcv 2605 . 2  |-  F/_ x A
2 nfv 1694 . 2  |-  F/ x ps
3 vtoclga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclga.2 . 2  |-  ( x  e.  B  ->  ph )
51, 2, 3, 4vtoclgaf 3158 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    e. wcel 1804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097
This theorem is referenced by:  vtoclri  3170  ssuni  4256  disjxiun  4434  opabiota  5921  fvmpt3  5944  fvmptss  5949  fnressn  6068  fressnfv  6070  caovord  6471  caovmo  6497  ordunisuc  6652  tfis3  6677  onfununi  7014  smogt  7040  tz7.44-1  7074  tz7.44-2  7075  tz7.44-3  7076  nnacl  7262  nnmcl  7263  nnecl  7264  nnacom  7268  nnaass  7273  nndi  7274  nnmass  7275  nnmsucr  7276  nnmcom  7277  nnmordi  7282  ixpfn  7477  findcard  7761  findcard2  7762  marypha1  7896  cantnfle  8093  cantnflem1  8111  cantnfleOLD  8123  cantnflem1OLD  8134  cnfcom  8147  cnfcomOLD  8155  fseqenlem1  8408  ackbij1lem5  8607  ackbij1lem8  8610  cardcf  8635  cfsmolem  8653  wunex2  9119  ingru  9196  recrecnq  9348  prlem934  9414  nn1suc  10563  uzind4s2  11151  rpnnen1  11222  cnref1o  11224  xmulasslem  11486  om2uzsuci  12038  expcl2lem  12157  hashmap  12472  hashpw  12473  seqcoll  12491  climub  13463  climserle  13464  sumrblem  13512  fsumcvg  13513  summolem2a  13516  infcvgaux2i  13648  divalglem8  13935  bezoutlem1  14053  alginv  14081  algcvg  14082  algcvga  14085  algfx  14086  isprm2lem  14101  prmind2  14105  prmpwdvds  14299  cnextfvval  20438  xrsxmet  21187  xrhmeo  21319  cmetcaulem  21600  bcth3  21643  itg2addlem  22038  taylfval  22626  sinord  22793  logexprlim  23372  lgsdir2lem4  23473  hlim2  25981  elnlfn  26719  lnconi  26824  chirredlem3  27183  chirredlem4  27184  cnre2csqlem  27765  eulerpartlemsf  28171  eulerpartlemn  28193  subfacp1lem1  28496  prodfn0  29003  prodfrec  29004  prodrblem  29036  fprodcvg  29037  prodmolem2a  29041  wfis3  29270  frins3  29306  wfr2  29335  findreccl  29893  mblfinlem3  30028  mblfinlem4  30029  ismblfin  30030  ftc1anclem3  30067  ftc1anclem8  30072  nn0prpwlem  30115  sdclem2  30210  iscringd  30371  zindbi  30857  fmuldfeq  31505  sumnnodd  31544  iblspltprt  31662  stoweidlem2  31673  stoweidlem17  31688  stoweidlem21  31692  stoweidlem43  31714  stoweidlem51  31722  wallispi  31741  bnj1321  33811  bnj1418  33824  renegclALT  34428
  Copyright terms: Public domain W3C validator