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	$⊢ A \in V$
	ceqsalv.2	$⊢ x = A \to (φ \leftrightarrow ψ)$
Assertion	ceqsalv	$⊢ \forall x (x = A \to φ) \leftrightarrow ψ$

Proof

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

Metamath Proof Explorer

Theorem ceqsalv

Proof