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

Theorem ceqsalv 3121
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  |-  A  e. 
_V
ceqsalv.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ceqsalv  |-  ( A. x ( x  =  A  ->  ph )  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem ceqsalv
StepHypRef Expression
1 nfv 1692 . 2  |-  F/ x ps
2 ceqsalv.1 . 2  |-  A  e. 
_V
3 ceqsalv.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3ceqsal 3120 1  |-  ( A. x ( x  =  A  ->  ph )  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1379    = wceq 1381    e. wcel 1802   _Vcvv 3093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-v 3095
This theorem is referenced by:  ralxpxfr2d  3208  clel2  3220  clel4  3223  reu8  3279  frsn  5057  raliunxp  5129  fv3  5866  funimass4  5906  marypha2lem3  7896  kmlem12  8541  fpwwe2lem12  9019  vdwmc2  14371  itg2leub  22011  nmoubi  25556  choc0  26113  nmopub  26696  nmfnleub  26713  heibor1lem  30277
  Copyright terms: Public domain W3C validator