Theorem nfeld 2909

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 1913	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2898	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2908	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2891	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1896	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2328	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1853	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

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

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 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783  df-cleq 2726  df-clel 2808  df-nfc 2884

This theorem is referenced by:  nfel  2912  nfneld  3044  nfrald  3355  ralcom2  3360  nfreuwOLD  3409  nfrmowOLD  3410  nfrmod  3415  nfreud  3416  nfrmo  3417  nfsbc1d  3788  nfsbcdw  3791  nfsbcd  3794  sbcrext  3853  nfdisjw  5102  nfdisj  5103  nfbrd  5169  nfriotadw  7377  nfriotad  7380  nfixpw  8937  nfixp  8938  axrepndlem2  10614  axrepnd  10615  axunnd  10617  axpowndlem2  10619  axpowndlem3  10620  axpowndlem4  10621  axpownd  10622  axregndlem2  10624  axinfndlem1  10626  axinfnd  10627  axacndlem4  10631  axacndlem5  10632  axacnd  10633  axnulg  35040