Theorem nfeld

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

	Ref	Expression
Hypotheses	nfeqd.1	|- ( ph -> F/_ x A )
	nfeqd.2	|- ( ph -> F/_ x B )
Assertion	nfeld	|- ( ph -> F/ x A e. B )

Proof

Step	Hyp	Ref	Expression
1		nfeqd.1	|- ( ph -> F/_ x A )
2		nfeqd.2	|- ( ph -> F/_ x B )
3		dfclel	|- ( A e. B <-> E. y ( y = A /\ y e. B ) )
4		nfv	|- F/ y ph
5		nfcvd	|- ( ph -> F/_ x y )
6	5 1	nfeqd	|- ( ph -> F/ x y = A )
7	2	nfcrd	|- ( ph -> F/ x y e. B )
8	6 7	nfand	|- ( ph -> F/ x ( y = A /\ y e. B ) )
9	4 8	nfexd	|- ( ph -> F/ x E. y ( y = A /\ y e. B ) )
10	3 9	nfxfrd	|- ( ph -> F/ x A e. B )