Theorem nfel1 2239

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

Hypothesis

Ref	Expression
nfeq1.1	|- F/_ x A

Assertion

Ref	Expression
nfel1	|- F/ x A e. B

Distinct variable group:   x, B

Allowed substitution hint:   A( x)

Proof of Theorem nfel1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 |- F/_ x A
2		nfcv 2228	. 2 |- F/_ x B
3	1, 2	nfel 2237	1 |- F/ x A e. B

Syntax hints:   F/wnf 1394   e. wcel 1438   F/_wnfc 2215

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-cleq 2081  df-clel 2084  df-nfc 2217

This theorem is referenced by:  vtocl2gf  2681  vtocl3gf  2682  vtoclgaf  2684  vtocl2gaf  2686  vtocl3gaf  2688  nfop  3638  pofun  4139  nfse  4168  rabxfrd  4291  mptfvex  5388  fvmptf  5395  fmptcof  5465  fliftfuns  5577  riota2f  5629  ovmpt2s  5768  ov2gf  5769  fmpt2x  5970  mpt2fvex  5973  qliftfuns  6374  xpf1o  6558  iunfidisj  6653  sumfct  10759  isumrblem  10761  isummolem3  10766  isummolem2a  10767  zisum  10770  fsumgcl  10773  fisum  10774  isumss  10779  isumss2  10781  fisumcvg2  10782  fsum3cvg2  10783  fsumsplitf  10798  isummulc2  10816  fsum2dlemstep  10824  fisumcom2  10828  fsumshftm  10835  fisum0diag2  10837  fsummulc2  10838  fsum00  10852  fsumabs  10855  fsumrelem  10861  fsumiun  10867  isumshft  10880  mertenslem2  10926  infssuzcldc  11221