Theorem ralsng

Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2015) Avoid ax-10 , ax-12 . (Revised by Gino Giotto, 30-Sep-2024)

	Ref	Expression
Hypothesis	ralsng.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ralsng	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\phi \leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ralsng.1	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		df-ral	$$⊢\forall x\in \left\{A\right\}\phi \leftrightarrow \forall x\left(x\in \left\{A\right\}\to \phi \right)$$
3		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
4	3	imbi1i	$$⊢\left(x\in \left\{A\right\}\to \phi \right)\leftrightarrow \left(x=A\to \phi \right)$$
5	4	albii	$$⊢\forall x\left(x\in \left\{A\right\}\to \phi \right)\leftrightarrow \forall x\left(x=A\to \phi \right)$$
6	2 5	bitri	$$⊢\forall x\in \left\{A\right\}\phi \leftrightarrow \forall x\left(x=A\to \phi \right)$$
7		elisset	$$⊢A\in V\to \exists xx=A$$
8	1	pm5.74i	$$⊢\left(x=A\to \phi \right)\leftrightarrow \left(x=A\to \psi \right)$$
9	8	albii	$$⊢\forall x\left(x=A\to \phi \right)\leftrightarrow \forall x\left(x=A\to \psi \right)$$
10	9	a1i	$$⊢\exists xx=A\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \forall x\left(x=A\to \psi \right)\right)$$
11		19.23v	$$⊢\forall x\left(x=A\to \psi \right)\leftrightarrow \left(\exists xx=A\to \psi \right)$$
12	11	a1i	$$⊢\exists xx=A\to \left(\forall x\left(x=A\to \psi \right)\leftrightarrow \left(\exists xx=A\to \psi \right)\right)$$
13		pm5.5	$$⊢\exists xx=A\to \left(\left(\exists xx=A\to \psi \right)\leftrightarrow \psi \right)$$
14	10 12 13	3bitrd	$$⊢\exists xx=A\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \psi \right)$$
15	7 14	syl	$$⊢A\in V\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \psi \right)$$
16	6 15	bitrid	$$⊢A\in V\to \left(\forall x\in \left\{A\right\}\phi \leftrightarrow \psi \right)$$