Theorem ceqsalv 3519

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   = wceq 1537  ∃wex 1776   ∈ wcel 2106  Vcvv 3478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814

This theorem is referenced by:  ceqsexv  3530  ralxpxfr2d  3646  frsn  5776  raliunxp  5853  idrefALT  6134  funimass4  6973  fnssintima  7382  imaeqalov  7672  marypha2lem3  9475  kmlem12  10200  vdwmc2  17013  itg2leub  25784  eqscut2  27866  addsuniflem  28049  mulsuniflem  28190  nmoubi  30801  choc0  31355  nmopub  31937  nmfnleub  31954  elintfv  35746  heibor1lem  37796  elmapintrab  43566