Theorem nfeld 2915

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 2812	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfv 1918	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2905	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2914	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2893	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1901	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2323	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1857	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ∃wex 1782  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-cleq 2725  df-clel 2811  df-nfc 2886

This theorem is referenced by:  nfel  2918  nfneld  3056  nfraldwOLD  3319  nfrald  3369  ralcom2  3374  nfreuwOLD  3423  nfrmowOLD  3424  nfrmod  3429  nfreud  3430  nfrmo  3431  nfsbc1d  3796  nfsbcdw  3799  nfsbcd  3802  sbcrext  3868  nfdisjw  5126  nfdisj  5127  nfbrd  5195  nfriotadw  7373  nfriotad  7377  nfixpw  8910  nfixp  8911  axrepndlem2  10588  axrepnd  10589  axunnd  10591  axpowndlem2  10593  axpowndlem3  10594  axpowndlem4  10595  axpownd  10596  axregndlem2  10598  axinfndlem1  10600  axinfnd  10601  axacndlem4  10605  axacndlem5  10606  axacnd  10607