Theorem nfel1 2240

Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq1.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfel1	⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Distinct variable group:   𝑥,𝐵

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfel1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2229	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2238	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1395   ∈ wcel 1439  Ⅎwnfc 2216

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-cleq 2082  df-clel 2085  df-nfc 2218

This theorem is referenced by:  vtocl2gf  2682  vtocl3gf  2683  vtoclgaf  2685  vtocl2gaf  2687  vtocl3gaf  2689  nfop  3644  pofun  4148  nfse  4177  rabxfrd  4304  mptfvex  5401  fvmptf  5408  fmptcof  5479  fliftfuns  5591  riota2f  5643  ovmpt2s  5782  ov2gf  5783  fmpt2x  5984  mpt2fvex  5987  qliftfuns  6390  xpf1o  6614  iunfidisj  6709  sumfct  10817  isumrblem  10819  isummolem3  10824  isummolem2a  10825  zisum  10828  fsumgcl  10831  fisum  10832  isumss  10837  isumss2  10839  fisumcvg2  10840  fsum3cvg2  10841  fsumsplitf  10856  isummulc2  10874  fsum2dlemstep  10882  fisumcom2  10886  fsumshftm  10893  fisum0diag2  10895  fsummulc2  10896  fsum00  10910  fsumabs  10913  fsumrelem  10919  fsumiun  10925  isumshft  10938  mertenslem2  10984  infssuzcldc  11279  iuncld  11869