Theorem elabgf

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of Quine p. 44. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003) (Revised by Mario Carneiro, 12-Oct-2016)

	Ref	Expression
Hypotheses	elabgf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	elabgf.2	$$⊢Ⅎx\psi$$
	elabgf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	elabgf	$$⊢A\in B\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elabgf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		elabgf.2	$$⊢Ⅎx\psi$$
3		elabgf.3	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
4		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\phi \right\}$$
5	1 4	nfel	$$⊢ℲxA\in \left\{x|\phi \right\}$$
6	5 2	nfbi	$$⊢Ⅎx\left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
7		eleq1	$$⊢x=A\to \left(x\in \left\{x|\phi \right\}\leftrightarrow A\in \left\{x|\phi \right\}\right)$$
8	7 3	bibi12d	$$⊢x=A\to \left(\left(x\in \left\{x|\phi \right\}\leftrightarrow \phi \right)\leftrightarrow \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)\right)$$
9		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
10	1 6 8 9	vtoclgf	$$⊢A\in B\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$