Theorem nfeld 2933

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 2836	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfv 1946	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2923	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2932	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2916	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1929	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2359	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1886	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ∃wex 1811  Ⅎwnf 1815   ∈ wcel 2144  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-cleq 2752  df-clel 2835  df-nfc 2909

This theorem is used by:  nfel  2936  nfneld  3070  nfrald  3357  ralcom2  3362  nfrmod  3408  nfreud  3409  nfrmo  3410  nfsbc1d  3756  nfsbcdw  3759  nfsbcd  3762  sbcrext  3820  nfdisj  5082  nfbrd  5150  nfriotadw  7389  nfriotad  7392  nfixpw  8952  nfixp  8953  axrepndlem2  10685  axrepnd  10686  axunnd  10688  axpowndlem2  10690  axpowndlem3  10691  axpowndlem4  10692  axpownd  10693  axregndlem2  10695  axinfndlem1  10697  axinfnd  10698  axacndlem4  10702  axacndlem5  10703  axacnd  10704  axsepg2  35876  axnulg  35881  axpowg2  35883  axpowg3  35884