Theorem elabf

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994) (Revised by Mario Carneiro, 12-Oct-2016)

	Ref	Expression
Hypotheses	elabf.1	$$⊢Ⅎx\psi$$
	elabf.2	$$⊢A\in \mathrm{V}$$
	elabf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	elabf	$$⊢A\in \left\{x|\phi \right\}\leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		elabf.1	$$⊢Ⅎx\psi$$
2		elabf.2	$$⊢A\in \mathrm{V}$$
3		elabf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
5	4 1 3	elabgf	$$⊢A\in \mathrm{V}\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
6	2 5	ax-mp	$$⊢A\in \left\{x|\phi \right\}\leftrightarrow \psi$$