Theorem nfel

Description: Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-1993) (Revised by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 16-Nov-2019)

	Ref	Expression
Hypotheses	nfnfc.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfeq.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfel	$$⊢ℲxA\in B$$

Proof

Step	Hyp	Ref	Expression
1		nfnfc.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfeq.2	$$⊢\underset{\_}{Ⅎ}xB$$
3	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
4	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xB$$
5	3 4	nfeld	$$⊢\top \to ℲxA\in B$$
6	5	mptru	$$⊢ℲxA\in B$$