Metamath Proof Explorer


Theorem ceqsalv

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 . (Revised by SN, 8-Sep-2024)

Ref Expression
Hypotheses ceqsalv.1 𝐴 ∈ V
ceqsalv.2 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
Assertion ceqsalv ( ∀ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ 𝜓 )

Proof

Step Hyp Ref Expression
1 ceqsalv.1 𝐴 ∈ V
2 ceqsalv.2 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
3 19.23v ( ∀ 𝑥 ( 𝑥 = 𝐴𝜓 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴𝜓 ) )
4 2 pm5.74i ( ( 𝑥 = 𝐴𝜑 ) ↔ ( 𝑥 = 𝐴𝜓 ) )
5 4 albii ( ∀ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴𝜓 ) )
6 1 isseti 𝑥 𝑥 = 𝐴
7 6 a1bi ( 𝜓 ↔ ( ∃ 𝑥 𝑥 = 𝐴𝜓 ) )
8 3 5 7 3bitr4i ( ∀ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ 𝜓 )