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

Theorem ceqsalv 3137
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 1707 . 2
2 ceqsalv.1 . 2
3 ceqsalv.2 . 2
41, 2, 3ceqsal 3136 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  e.wcel 1818   cvv 3109
This theorem is referenced by:  ralxpxfr2d  3224  clel2  3236  clel4  3239  reu8  3295  frsn  5075  raliunxp  5147  fv3  5884  funimass4  5924  marypha2lem3  7917  kmlem12  8562  fpwwe2lem12  9040  vdwmc2  14497  itg2leub  22141  nmoubi  25687  choc0  26244  nmopub  26827  nmfnleub  26844  heibor1lem  30305
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-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator