Theorem nfeld 2913

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 1917	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2903	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2912	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2891	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1900	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2322	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1856	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  ∃wex 1781  Ⅎwnf 1785   ∈ wcel 2106  Ⅎwnfc 2882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-cleq 2723  df-clel 2809  df-nfc 2884

This theorem is referenced by:  nfel  2916  nfneld  3054  nfraldwOLD  3300  nfrald  3343  ralcom2  3348  nfreuwOLD  3395  nfrmowOLD  3396  nfrmod  3401  nfreud  3402  nfrmo  3403  nfsbc1d  3760  nfsbcdw  3763  nfsbcd  3766  sbcrext  3832  nfdisjw  5087  nfdisj  5088  nfbrd  5156  nfriotadw  7326  nfriotad  7330  nfixpw  8861  nfixp  8862  axrepndlem2  10538  axrepnd  10539  axunnd  10541  axpowndlem2  10543  axpowndlem3  10544  axpowndlem4  10545  axpownd  10546  axregndlem2  10548  axinfndlem1  10550  axinfnd  10551  axacndlem4  10555  axacndlem5  10556  axacnd  10557