ceqsal

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 df-clab . (Revised by Wolf Lammen, 23-Jan-2025)

	Ref	Expression
Hypotheses	ceqsal.1	$⊢ Ⅎ x ψ$
	ceqsal.2	$⊢ A \in V$
	ceqsal.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	ceqsal	$⊢ \forall x (x = A \to φ) \leftrightarrow ψ$

Proof

Step	Hyp	Ref	Expression
1		ceqsal.1	$⊢ Ⅎ x ψ$
2		ceqsal.2	$⊢ A \in V$
3		ceqsal.3	$⊢ x = A \to (φ \leftrightarrow ψ)$
4	1	19.23	$⊢ \forall x (x = A \to ψ) \leftrightarrow (\exists x x = A \to ψ)$
5	3	pm5.74i	$⊢ (x = A \to φ) \leftrightarrow (x = A \to ψ)$
6	5	albii	$⊢ \forall x (x = A \to φ) \leftrightarrow \forall x (x = A \to ψ)$
7	2	isseti	$⊢ \exists x x = A$
8	7	a1bi	$⊢ ψ \leftrightarrow (\exists x x = A \to ψ)$
9	4 6 8	3bitr4i	$⊢ \forall x (x = A \to φ) \leftrightarrow ψ$

Metamath Proof Explorer

Theorem ceqsal

Proof