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

Theorem ceqsalv 3075
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 1722 . 2  |-  F/ x ps
2 ceqsalv.1 . 2  |-  A  e. 
_V
3 ceqsalv.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3ceqsal 3074 1  |-  ( A. x ( x  =  A  ->  ph )  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1397    = wceq 1399    e. wcel 1836   _Vcvv 3047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-12 1872  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-v 3049
This theorem is referenced by:  ralxpxfr2d  3162  clel2  3174  clel4  3177  reu8  3233  frsn  4997  raliunxp  5068  fv3  5800  funimass4  5838  marypha2lem3  7830  kmlem12  8472  fpwwe2lem12  8948  vdwmc2  14518  itg2leub  22245  nmoubi  25825  choc0  26382  nmopub  26964  nmfnleub  26981  heibor1lem  30507
  Copyright terms: Public domain W3C validator