Theorem ceqsalv 3467

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 2171. (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		ceqsalv.2	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	pm5.74i 270	. . 3 ⊢ ((𝑥 = 𝐴 → 𝜑) ↔ (𝑥 = 𝐴 → 𝜓))
3	2	albii 1822	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
4		19.23v 1945	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
5		ceqsalv.1	. . . 4 ⊢ 𝐴 ∈ V
6	5	isseti 3447	. . 3 ⊢ ∃𝑥 𝑥 = 𝐴
7		pm5.5 362	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
8	6, 7	ax-mp 5	. 2 ⊢ ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓)
9	3, 4, 8	3bitri 297	1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2816

This theorem is referenced by:  ralxpxfr2d  3576  clel4OLD  3595  frsn  5674  raliunxp  5748  idrefALT  6018  funimass4  6834  marypha2lem3  9196  kmlem12  9917  vdwmc2  16680  itg2leub  24899  nmoubi  29134  choc0  29688  nmopub  30270  nmfnleub  30287  fnssintima  33676  elintfv  33738  eqscut2  34000  heibor1lem  35967  elmapintrab  41184