Theorem nfeld 2912

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539  ∃wex 1779  Ⅎwnf 1783   ∈ wcel 2104  Ⅎwnfc 2881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-nf 1784  df-cleq 2722  df-clel 2808  df-nfc 2883

This theorem is referenced by:  nfel  2915  nfneld  3053  nfraldwOLD  3316  nfrald  3366  ralcom2  3371  nfreuwOLD  3420  nfrmowOLD  3421  nfrmod  3426  nfreud  3427  nfrmo  3428  nfsbc1d  3796  nfsbcdw  3799  nfsbcd  3802  sbcrext  3868  nfdisjw  5126  nfdisj  5127  nfbrd  5195  nfriotadw  7377  nfriotad  7381  nfixpw  8914  nfixp  8915  axrepndlem2  10592  axrepnd  10593  axunnd  10595  axpowndlem2  10597  axpowndlem3  10598  axpowndlem4  10599  axpownd  10600  axregndlem2  10602  axinfndlem1  10604  axinfnd  10605  axacndlem4  10609  axacndlem5  10610  axacnd  10611