Theorem nfeld

Description: Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016)

	Ref	Expression
Hypotheses	nfeqd.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfeqd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	nfeld	$$⊢\phi \to ℲxA\in B$$

Proof

Step	Hyp	Ref	Expression
1		nfeqd.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfeqd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
3		dfclel	$$⊢A\in B\leftrightarrow \exists y\left(y=A\wedge y\in B\right)$$
4		nfv	$$⊢Ⅎy\phi$$
5		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}xy$$
6	5 1	nfeqd	$$⊢\phi \to Ⅎxy=A$$
7	2	nfcrd	$$⊢\phi \to Ⅎxy\in B$$
8	6 7	nfand	$$⊢\phi \to Ⅎx\left(y=A\wedge y\in B\right)$$
9	4 8	nfexd	$$⊢\phi \to Ⅎx\exists y\left(y=A\wedge y\in B\right)$$
10	3 9	nfxfrd	$$⊢\phi \to ℲxA\in B$$