Theorem ceqsalv 3493

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 2212. (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 1971	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
2		ceqsalv.2	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 274	. . 3 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
4	3	albii 1848	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
5		ceqsalv.1	. . . 4 ⊢ 𝐴 ∈ V
6	5	isseti 3472	. . 3 ⊢ ∃𝑥 𝑥 = 𝐴
7	6	a1bi 365	. 2 ⊢ (𝜓 ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
8	1, 4, 7	3bitr4i 306	1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569  ∃wex 1808   ∈ wcel 2142  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-clel 2837

This theorem is used by:  ceqsexv  3502  ralxpxfr2d  3604  frsn  5748  raliunxp  5824  idrefALT  6112  funimass4  6945  fnssintima  7362  imaeqalov  7651  marypha2lem3  9395  kmlem12  10152  vdwmc2  17045  itg2leub  25904  eqcuts2  27990  addsuniflem  28205  mulsuniflem  28353  onsfi  28560  nmoubi  31135  choc0  31689  nmopub  32271  nmfnleub  32288  elintfv  36265  heibor1lem  38488  elmapintrab  44330