Theorem ceqsalv 3457

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 2173. (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 1823	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜓))
4		19.23v 1946	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓))
5		ceqsalv.1	. . . 4 ⊢ 𝐴 ∈ V
6	5	isseti 3437	. . 3 ⊢ ∃𝑥 𝑥 = 𝐴
7		pm5.5 361	. . 3 ⊢ (∃𝑥 𝑥 = 𝐴 → ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓))
8	6, 7	ax-mp 5	. 2 ⊢ ((∃𝑥 𝑥 = 𝐴 → 𝜓) ↔ 𝜓)
9	3, 4, 8	3bitri 296	1 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝜑) ↔ 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-clel 2817

This theorem is referenced by:  ralxpxfr2d  3568  clel4OLD  3588  frsn  5665  raliunxp  5737  idrefALT  6007  funimass4  6816  marypha2lem3  9126  kmlem12  9848  vdwmc2  16608  itg2leub  24804  nmoubi  29035  choc0  29589  nmopub  30171  nmfnleub  30188  fnssintima  33578  elintfv  33644  eqscut2  33927  heibor1lem  35894  elmapintrab  41073