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 e. V -> ( A. x ( x = A -> ph ) <-> E. x ( x = A /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq2	|- ( y = A -> ( x = y <-> x = A ) )
2	1	anbi1d	|- ( y = A -> ( ( x = y /\ ph ) <-> ( x = A /\ ph ) ) )
3	2	exbidv	|- ( y = A -> ( E. x ( x = y /\ ph ) <-> E. x ( x = A /\ ph ) ) )
4	1	imbi1d	|- ( y = A -> ( ( x = y -> ph ) <-> ( x = A -> ph ) ) )
5	4	albidv	|- ( y = A -> ( A. x ( x = y -> ph ) <-> A. x ( x = A -> ph ) ) )
6		sbalex	|- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )
7	3 5 6	vtoclbg	|- ( A e. V -> ( E. x ( x = A /\ ph ) <-> A. x ( x = A -> ph ) ) )
8	7	bicomd	|- ( A e. V -> ( A. x ( x = A -> ph ) <-> E. x ( x = A /\ ph ) ) )