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

Theorem vtoclga 3465
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
Hypotheses
Ref Expression
vtoclga.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclga.2 (𝑥𝐵𝜑)
Assertion
Ref Expression
vtoclga (𝐴𝐵𝜓)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtoclga
StepHypRef Expression
1 nfcv 2948 . 2 𝑥𝐴
2 nfv 2005 . 2 𝑥𝜓
3 vtoclga.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtoclga.2 . 2 (𝑥𝐵𝜑)
51, 2, 3, 4vtoclgaf 3464 1 (𝐴𝐵𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wcel 2156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393
This theorem is referenced by:  vtoclri  3476  disjxiun  4841  wfis3  5934  opabiota  6482  fvmpt3  6507  fvmptss  6513  fnressn  6649  fressnfv  6651  caovord  7075  caovmo  7101  ordunisuc  7262  tfis3  7287  wfr2a  7668  onfununi  7674  smogt  7700  tz7.44-1  7738  tz7.44-2  7739  tz7.44-3  7740  nnacl  7928  nnmcl  7929  nnecl  7930  nnacom  7934  nnaass  7939  nndi  7940  nnmass  7941  nnmsucr  7942  nnmcom  7943  nnmordi  7948  ixpfn  8151  findcard  8438  findcard2  8439  marypha1  8579  cantnfle  8815  cantnflem1  8833  cnfcom  8844  fseqenlem1  9130  ackbij1lem8  9334  cardcf  9359  cfsmolem  9377  wunex2  9845  ingru  9922  recrecnq  10074  prlem934  10140  nn1suc  11326  uzind4s2  11967  rpnnen1lem6  12038  cnref1o  12041  xmulasslem  12333  om2uzsuci  12971  expcl2lem  13095  hashpw  13440  seqcoll  13465  climub  14615  climserle  14616  sumrblem  14665  fsumcvg  14666  summolem2a  14669  infcvgaux2i  14812  prodfn0  14847  prodfrec  14848  prodrblem  14880  fprodcvg  14881  prodmolem2a  14885  divalglem8  15343  bezoutlem1  15475  alginv  15507  algcvg  15508  algcvga  15511  algfx  15512  prmind2  15616  prmpwdvds  15825  cnextfvval  22082  xrsxmet  22825  xrhmeo  22958  cmetcaulem  23298  bcth3  23340  itg2addlem  23739  taylfval  24327  sinord  24495  logexprlim  25164  lgsdir2lem4  25267  hlim2  28377  elnlfn  29115  lnconi  29220  chirredlem3  29579  chirredlem4  29580  cnre2csqlem  30281  eulerpartlemsf  30746  eulerpartlemn  30768  bnj1321  31418  bnj1418  31431  subfacp1lem1  31484  frins3  32072  nn0prpwlem  32638  findreccl  32769  mptsnunlem  33502  rdgeqoa  33534  poimirlem22  33744  poimirlem26  33748  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  ftc1anclem3  33799  ftc1anclem8  33804  sdclem2  33849  iscringd  34108  renegclALT  34742  zindbi  38012  fmuldfeq  40295  sumnnodd  40342  iblspltprt  40668  stoweidlem2  40698  stoweidlem17  40713  stoweidlem21  40717  stoweidlem43  40739  stoweidlem51  40747  wallispi  40766
  Copyright terms: Public domain W3C validator