Theorem ceqsalv 3495

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 2214. (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 1964	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
2		ceqsalv.2	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 273	. . 3 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
4	3	albii 1841	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
5		ceqsalv.1	. . . 4 ⊢ 𝐴 ∈ V
6	5	isseti 3474	. . 3 ⊢ ∃𝑥 𝑥 = 𝐴
7	6	a1bi 364	. 2 ⊢ (𝜓 ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
8	1, 4, 7	3bitr4i 305	1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1560   = wceq 1562  ∃wex 1801   ∈ wcel 2144  Vcvv 3456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-clel 2839

This theorem is referenced by:  ceqsexv  3504  ralxpxfr2d  3607  frsn  5737  raliunxp  5813  idrefALT  6102  funimass4  6933  fnssintima  7348  imaeqalov  7637  marypha2lem3  9385  kmlem12  10120  vdwmc2  17017  itg2leub  25798  eqcuts2  27881  addsuniflem  28096  mulsuniflem  28244  onsfi  28451  nmoubi  30977  choc0  31531  nmopub  32113  nmfnleub  32130  elintfv  36120  heibor1lem  38313  elmapintrab  44157