Theorem nfeld 2917

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 2817	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfv 1914	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2906	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2916	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2899	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1897	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2330	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1853	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∃wex 1778  Ⅎwnf 1782   ∈ wcel 2108  Ⅎwnfc 2890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1779  df-nf 1783  df-cleq 2729  df-clel 2816  df-nfc 2892

This theorem is referenced by:  nfel  2920  nfneld  3055  nfrald  3372  ralcom2  3377  nfreuwOLD  3426  nfrmowOLD  3427  nfrmod  3432  nfreud  3433  nfrmo  3434  nfsbc1d  3812  nfsbcdw  3815  nfsbcd  3818  sbcrext  3885  nfdisjw  5130  nfdisj  5131  nfbrd  5197  nfriotadw  7403  nfriotad  7406  nfixpw  8964  nfixp  8965  axrepndlem2  10640  axrepnd  10641  axunnd  10643  axpowndlem2  10645  axpowndlem3  10646  axpowndlem4  10647  axpownd  10648  axregndlem2  10650  axinfndlem1  10652  axinfnd  10653  axacndlem4  10657  axacndlem5  10658  axacnd  10659  axnulg  35099