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

Theorem vtoclga 3142
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 2616 . 2  |-  F/_ x A
2 nfv 1674 . 2  |-  F/ x ps
3 vtoclga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclga.2 . 2  |-  ( x  e.  B  ->  ph )
51, 2, 3, 4vtoclgaf 3141 1  |-  ( A  e.  B  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080
This theorem is referenced by:  vtoclri  3153  ssuni  4224  disjxiun  4400  opabiota  5866  fvmpt3  5889  fvmptss  5894  fnressn  6006  fressnfv  6008  caovord  6387  caovmo  6413  ordunisuc  6556  tfis3  6581  onfununi  6915  smogt  6941  tfrlem1  6948  tz7.44-1  6975  tz7.44-2  6976  tz7.44-3  6977  nnacl  7163  nnmcl  7164  nnecl  7165  nnacom  7169  nnaass  7174  nndi  7175  nnmass  7176  nnmsucr  7177  nnmcom  7178  nnmordi  7183  ixpfn  7382  findcard  7665  findcard2  7666  marypha1  7799  cantnfle  7994  cantnflem1  8012  cantnfleOLD  8024  cantnflem1OLD  8035  cnfcom  8048  cnfcomOLD  8056  fseqenlem1  8309  ackbij1lem5  8508  ackbij1lem8  8511  cardcf  8536  cfsmolem  8554  wunex2  9020  ingru  9097  recrecnq  9251  prlem934  9317  nn1suc  10458  uzind4s2  11030  rpnnen1  11099  cnref1o  11101  xmulasslem  11363  om2uzsuci  11892  expcl2lem  11998  hashmap  12319  hashpw  12320  seqcoll  12338  climub  13261  climserle  13262  sumrblem  13310  fsumcvg  13311  summolem2a  13314  infcvgaux2i  13442  divalglem8  13726  bezoutlem1  13844  alginv  13872  algcvg  13873  algcvga  13876  algfx  13877  isprm2lem  13892  prmind2  13896  prmpwdvds  14087  cnextfvval  19779  xrsxmet  20528  xrhmeo  20660  cmetcaulem  20941  bcth3  20984  itg2addlem  21379  taylfval  21967  sinord  22133  logexprlim  22707  lgsdir2lem4  22808  hlim2  24773  elnlfn  25511  lnconi  25616  chirredlem3  25975  chirredlem4  25976  cnre2csqlem  26508  eulerpartlemsf  26909  eulerpartlemn  26931  subfacp1lem1  27234  prodfn0  27576  prodfrec  27577  prodrblem  27609  fprodcvg  27610  prodmolem2a  27614  wfis3  27843  frins3  27879  wfr2  27908  findreccl  28466  mblfinlem3  28601  mblfinlem4  28602  ismblfin  28603  ftc1anclem3  28640  ftc1anclem8  28645  nn0prpwlem  28688  sdclem2  28809  iscringd  28970  zindbi  29458  fmuldfeq  29935  stoweidlem2  29968  stoweidlem17  29983  stoweidlem21  29987  stoweidlem43  30009  stoweidlem51  30017  wallispi  30036  bnj1321  32373  bnj1418  32386  renegclALT  32977
  Copyright terms: Public domain W3C validator