Theorem ceqsalv 3472

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1546   = wceq 1548  ∃wex 1787   ∈ wcel 2121  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-clel 2816

This theorem is referenced by:  ceqsexv  3481  ralxpxfr2d  3586  frsn  5709  raliunxp  5784  idrefALT  6070  funimass4  6895  fnssintima  7310  imaeqalov  7599  marypha2lem3  9344  kmlem12  10079  vdwmc2  16945  itg2leub  25723  eqcuts2  27800  addsuniflem  28015  mulsuniflem  28163  onsfi  28370  nmoubi  30865  choc0  31419  nmopub  32001  nmfnleub  32018  elintfv  36008  heibor1lem  38191  elmapintrab  44035