Theorem nfeld 2908

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 2810	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfv 1915	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2897	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2907	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2890	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1898	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2332	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1855	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ∃wex 1780  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-cleq 2726  df-clel 2809  df-nfc 2883

This theorem is referenced by:  nfel  2911  nfneld  3043  nfrald  3340  ralcom2  3345  nfrmod  3393  nfreud  3394  nfrmo  3395  nfsbc1d  3756  nfsbcdw  3759  nfsbcd  3762  sbcrext  3821  nfdisjw  5075  nfdisj  5076  nfbrd  5142  nfriotadw  7321  nfriotad  7324  nfixpw  8852  nfixp  8853  axrepndlem2  10502  axrepnd  10503  axunnd  10505  axpowndlem2  10507  axpowndlem3  10508  axpowndlem4  10509  axpownd  10510  axregndlem2  10512  axinfndlem1  10514  axinfnd  10515  axacndlem4  10519  axacndlem5  10520  axacnd  10521  axnulg  35213