Theorem elab3

Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000)

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

Proof

Step	Hyp	Ref	Expression
1		elab3.1	$$⊢\psi \to A\in \mathrm{V}$$
2		elab3.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
3	2	elab3g	$$⊢\left(\psi \to A\in \mathrm{V}\right)\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
4	1 3	ax-mp	$$⊢A\in \left\{x|\phi \right\}\leftrightarrow \psi$$