Theorem nfeld 2936

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 2839	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfv 1944	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2926	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2935	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2919	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1927	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2362	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1884	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  ∃wex 1809  Ⅎwnf 1813   ∈ wcel 2143  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-cleq 2755  df-clel 2838  df-nfc 2912

This theorem is referenced by:  nfel  2939  nfneld  3073  nfrald  3361  ralcom2  3366  nfrmod  3412  nfreud  3413  nfrmo  3414  nfsbc1d  3762  nfsbcdw  3765  nfsbcd  3768  sbcrext  3826  nfdisj  5089  nfbrd  5157  nfriotadw  7375  nfriotad  7378  nfixpw  8910  nfixp  8911  axrepndlem2  10573  axrepnd  10574  axunnd  10576  axpowndlem2  10578  axpowndlem3  10579  axpowndlem4  10580  axpownd  10581  axregndlem2  10583  axinfndlem1  10585  axinfnd  10586  axacndlem4  10590  axacndlem5  10591  axacnd  10592  axsepg2  35553  axnulg  35558  axpowg2  35560  axpowg3  35561