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

Theorem ceqsalv 3109
Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.)
Hypotheses
Ref Expression
ceqsalv.1
ceqsalv.2
Assertion
Ref Expression
ceqsalv
Distinct variable groups:   ,   ,

Proof of Theorem ceqsalv
StepHypRef Expression
1 nfv 1674 . 2
2 ceqsalv.1 . 2
3 ceqsalv.2 . 2
41, 2, 3ceqsal 3108 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1368  =wceq 1370  e.wcel 1758   cvv 3081
This theorem is referenced by:  ralxpxfr2d  3194  clel2  3206  clel4  3209  reu8  3265  frsn  5026  raliunxp  5096  fv3  5826  funimass4  5865  marypha2lem3  7823  kmlem12  8467  fpwwe2lem12  8945  vdwmc2  14198  itg2leub  21612  nmoubi  24641  choc0  25198  nmopub  25781  nmfnleub  25798  heibor1lem  29168
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-12 1794  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-v 3083
  Copyright terms: Public domain W3C validator