NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ceqsalv GIF version

Theorem ceqsalv 2885
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 V
ceqsalv.2 (x = A → (φψ))
Assertion
Ref Expression
ceqsalv (x(x = Aφ) ↔ ψ)
Distinct variable groups:   x,A   ψ,x
Allowed substitution hint:   φ(x)

Proof of Theorem ceqsalv
StepHypRef Expression
1 nfv 1619 . 2 xψ
2 ceqsalv.1 . 2 A V
3 ceqsalv.2 . 2 (x = A → (φψ))
41, 2, 3ceqsal 2884 1 (x(x = Aφ) ↔ ψ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176  wal 1540   = wceq 1642   wcel 1710  Vcvv 2859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861
This theorem is referenced by:  clel2  2975  clel4  2978  reu8  3032  eqpw1  4162  pw111  4170  ssrelk  4211  eqrelk  4212  elp6  4263  sikexlem  4295  insklem  4304  nnadjoin  4520  nnadjoinpw  4521  nnpweq  4523  tfinnn  4534  raliunxp  4823  ssopr  4846  intirr  5029  fv3  5341  funimass4  5368  dfnnc3  5885  spacind  6287
  Copyright terms: Public domain W3C validator