Theorem nfeld 2903

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 2803	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
2		nfv 1909	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfcvd 2892	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝑦)
4		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
5	3, 4	nfeqd 2902	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
7	6	nfcrd 2884	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
8	5, 7	nfand 1892	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
9	2, 8	nfexd 2317	. 2 ⊢ (𝜑 → Ⅎ𝑥∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵))
10	1, 9	nfxfrd 1848	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533  ∃wex 1773  Ⅎwnf 1777   ∈ wcel 2098  Ⅎwnfc 2875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778  df-cleq 2717  df-clel 2802  df-nfc 2877

This theorem is referenced by:  nfel  2906  nfneld  3044  nfraldwOLD  3308  nfrald  3355  ralcom2  3360  nfreuwOLD  3408  nfrmowOLD  3409  nfrmod  3414  nfreud  3415  nfrmo  3416  nfsbc1d  3791  nfsbcdw  3794  nfsbcd  3797  sbcrext  3863  nfdisjw  5126  nfdisj  5127  nfbrd  5195  nfriotadw  7383  nfriotad  7387  nfixpw  8935  nfixp  8936  axrepndlem2  10623  axrepnd  10624  axunnd  10626  axpowndlem2  10628  axpowndlem3  10629  axpowndlem4  10630  axpownd  10631  axregndlem2  10633  axinfndlem1  10635  axinfnd  10636  axacndlem4  10640  axacndlem5  10641  axacnd  10642