Theorem ceqsalv 3469

Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.) Avoid ax-12 2185. (Revised by SN, 8-Sep-2024.)

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		19.23v 1944	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
2		ceqsalv.2	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 271	. . 3 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
4	3	albii 1821	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
5		ceqsalv.1	. . . 4 ⊢ 𝐴 ∈ V
6	5	isseti 3447	. . 3 ⊢ ∃𝑥 𝑥 = 𝐴
7	6	a1bi 362	. 2 ⊢ (𝜓 ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
8	1, 4, 7	3bitr4i 303	1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811

This theorem is referenced by:  ceqsexv  3478  ralxpxfr2d  3588  frsn  5719  raliunxp  5794  idrefALT  6076  funimass4  6904  fnssintima  7317  imaeqalov  7606  marypha2lem3  9350  kmlem12  10084  vdwmc2  16950  itg2leub  25701  eqcuts2  27778  addsuniflem  27993  mulsuniflem  28141  onsfi  28348  nmoubi  30843  choc0  31397  nmopub  31979  nmfnleub  31996  elintfv  35947  heibor1lem  38130  elmapintrab  44003