Theorem nfeld

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

	Ref	Expression
Hypotheses	nfeqd.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfeqd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
Assertion	nfeld	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfeqd.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfeqd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
3		dfclel	⊢ ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
4		nfv	⊢ Ⅎ 𝑦 𝜑
5		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 )
6	5 1	nfeqd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 = 𝐴 )
7	2	nfcrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐵 )
8	6 7	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
9	4 8	nfexd	⊢ ( 𝜑 → Ⅎ 𝑥 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
10	3 9	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 ∈ 𝐵 )