Theorem nfeld 2942

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

Hypotheses

Ref	Expression
nfeqd.1	⊢ (𝜑 → Ⅎ𝑥𝐴)
nfeqd.2	⊢ (𝜑 → Ⅎ𝑥𝐵)

Assertion

Ref	Expression
nfeld	⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

Proof of Theorem nfeld

Dummy variable 𝑦 is distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ∃wex 1806  Ⅎwnf 1810   ∈ wcel 2149  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811  df-cleq 2761  df-clel 2844  df-nfc 2918

This theorem is referenced by:  nfel  2945  nfneld  3079  nfrald  3368  ralcom2  3373  nfrmod  3419  nfreud  3420  nfrmo  3421  nfsbc1d  3771  nfsbcdw  3774  nfsbcd  3777  sbcrext  3835  nfdisj  5093  nfbrd  5161  nfriotadw  7376  nfriotad  7379  nfixpw  8914  nfixp  8915  axrepndlem2  10578  axrepnd  10579  axunnd  10581  axpowndlem2  10583  axpowndlem3  10584  axpowndlem4  10585  axpownd  10586  axregndlem2  10588  axinfndlem1  10590  axinfnd  10591  axacndlem4  10595  axacndlem5  10596  axacnd  10597  axsepg2  35476  axnulg  35481  axpowg2  35483  axpowg3  35484