This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ceqsalg

Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. For an alternate proof, see ceqsalgALT . (Contributed by NM, 29-Oct-2003) (Proof shortened by BJ, 29-Sep-2019)

Ref Expression
Hypotheses ceqsalg.1 ⊢ Ⅎ x ψ
ceqsalg.2 ⊢ x = A → φ ↔ ψ
Assertion ceqsalg ⊢ A ∈ V → ∀ x x = A → φ ↔ ψ

Proof

Step Hyp Ref Expression
1 ceqsalg.1 ⊢ Ⅎ x ψ
2 ceqsalg.2 ⊢ x = A → φ ↔ ψ
3 2 ax-gen ⊢ ∀ x x = A → φ ↔ ψ
4 ceqsalt ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ ↔ ψ
5 1 3 4 mp3an12 ⊢ A ∈ V → ∀ x x = A → φ ↔ ψ