Theorem alexeqg

Description: Two ways to express substitution of A for x in ph . This is the analogue for classes of sbalex . (Contributed by NM, 2-Mar-1995) (Revised by BJ, 27-Apr-2019)

	Ref	Expression
Assertion	alexeqg	$$⊢A\in V\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \exists x\left(x=A\wedge \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq2	$$⊢y=A\to \left(x=y\leftrightarrow x=A\right)$$
2	1	anbi1d	$$⊢y=A\to \left(\left(x=y\wedge \phi \right)\leftrightarrow \left(x=A\wedge \phi \right)\right)$$
3	2	exbidv	$$⊢y=A\to \left(\exists x\left(x=y\wedge \phi \right)\leftrightarrow \exists x\left(x=A\wedge \phi \right)\right)$$
4	1	imbi1d	$$⊢y=A\to \left(\left(x=y\to \phi \right)\leftrightarrow \left(x=A\to \phi \right)\right)$$
5	4	albidv	$$⊢y=A\to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
6		sbalex	$$⊢\exists x\left(x=y\wedge \phi \right)\leftrightarrow \forall x\left(x=y\to \phi \right)$$
7	3 5 6	vtoclbg	$$⊢A\in V\to \left(\exists x\left(x=A\wedge \phi \right)\leftrightarrow \forall x\left(x=A\to \phi \right)\right)$$
8	7	bicomd	$$⊢A\in V\to \left(\forall x\left(x=A\to \phi \right)\leftrightarrow \exists x\left(x=A\wedge \phi \right)\right)$$