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

Theorem ceqsalv 2989
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 1672 . 2  |-  F/ x ps
2 ceqsalv.1 . 2  |-  A  e. 
_V
3 ceqsalv.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3ceqsal 2988 1  |-  ( A. x ( x  =  A  ->  ph )  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1360    = wceq 1362    e. wcel 1755   _Vcvv 2962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964
This theorem is referenced by:  ralxpxfr2d  3073  clel2  3085  clel4  3088  reu8  3144  frsn  4896  raliunxp  4966  fv3  5691  funimass4  5730  marypha2lem3  7675  kmlem12  8318  fpwwe2lem12  8796  vdwmc2  14023  itg2leub  21054  nmoubi  23995  choc0  24552  nmopub  25135  nmfnleub  25152  heibor1lem  28552
  Copyright terms: Public domain W3C validator