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

Theorem ceqsalv 3373
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 𝐴 ∈ V
ceqsalv.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ceqsalv (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ceqsalv
StepHypRef Expression
1 nfv 1992 . 2 𝑥𝜓
2 ceqsalv.1 . 2 𝐴 ∈ V
3 ceqsalv.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
41, 2, 3ceqsal 3372 1 (∀𝑥(𝑥 = 𝐴𝜑) ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1630   = wceq 1632  wcel 2139  Vcvv 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-12 2196  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-v 3342
This theorem is referenced by:  ralxpxfr2d  3466  clel4  3482  frsn  5346  raliunxp  5417  fv3  6367  funimass4  6409  marypha2lem3  8508  kmlem12  9175  fpwwe2lem12  9655  vdwmc2  15885  itg2leub  23700  nmoubi  27936  choc0  28494  nmopub  29076  nmfnleub  29093  elintfv  31969  heibor1lem  33921  elmapintrab  38384
  Copyright terms: Public domain W3C validator