Theorem nfeld 2935

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 2838	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfv 1934	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2925	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2934	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2918	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1917	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2361	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1874	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560  ∃wex 1799  Ⅎwnf 1803   ∈ wcel 2142  Ⅎwnfc 2909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1800  df-nf 1804  df-cleq 2754  df-clel 2837  df-nfc 2911

This theorem is referenced by:  nfel  2938  nfneld  3070  nfrald  3359  ralcom2  3364  nfrmod  3410  nfreud  3411  nfrmo  3412  nfsbc1d  3762  nfsbcdw  3765  nfsbcd  3768  sbcrext  3826  nfdisj  5080  nfbrd  5146  nfriotadw  7361  nfriotad  7364  nfixpw  8898  nfixp  8899  axrepndlem2  10551  axrepnd  10552  axunnd  10554  axpowndlem2  10556  axpowndlem3  10557  axpowndlem4  10558  axpownd  10559  axregndlem2  10561  axinfndlem1  10563  axinfnd  10564  axacndlem4  10568  axacndlem5  10569  axacnd  10570  axsepg2  35436  axnulg  35441  axpowg2  35443  axpowg3  35444