Theorem ceqsalv 3529

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

Step	Hyp	Ref	Expression
1		nfv 1914	. 2 ⊢ Ⅎ𝑥𝜓
2		ceqsalv.1	. 2 ⊢ 𝐴 ∈ V
3		ceqsalv.2	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	ceqsal 3528	1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1534   = wceq 1536   ∈ wcel 2113  Vcvv 3491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1084  df-ex 1780  df-nf 1784  df-cleq 2813  df-clel 2892

This theorem is referenced by:  ralxpxfr2d  3636  clel4  3653  frsn  5632  raliunxp  5703  idrefALT  5966  funimass4  6723  marypha2lem3  8894  kmlem12  9580  vdwmc2  16310  itg2leub  24330  nmoubi  28547  choc0  29101  nmopub  29683  nmfnleub  29700  elintfv  33028  heibor1lem  35120  elmapintrab  40010