Theorem nfel1 2293

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 2282	. 2 |- F/_ x B
3	1, 2	nfel 2291	1 |- F/ x A e. B

Syntax hints:   F/wnf 1437   e. wcel 1481   F/_wnfc 2269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-cleq 2133  df-clel 2136  df-nfc 2271

This theorem is referenced by:  vtocl2gf  2751  vtocl3gf  2752  vtoclgaf  2754  vtocl2gaf  2756  vtocl3gaf  2758  nfop  3729  pofun  4242  nfse  4271  rabxfrd  4398  mptfvex  5514  fvmptf  5521  fmptcof  5595  fliftfuns  5707  riota2f  5759  ovmpos  5902  ov2gf  5903  fmpox  6106  mpofvex  6109  qliftfuns  6521  xpf1o  6746  iunfidisj  6842  cc3  7100  sumfct  11175  sumrbdclem  11178  summodclem3  11181  summodclem2a  11182  zsumdc  11185  fsumgcl  11187  fsum3  11188  isumss  11192  isumss2  11194  fsum3cvg2  11195  fsumsplitf  11209  fsum2dlemstep  11235  fisumcom2  11239  fsumshftm  11246  fisum0diag2  11248  fsummulc2  11249  fsum00  11263  fsumabs  11266  fsumrelem  11272  fsumiun  11278  isumshft  11291  mertenslem2  11337  prodrbdclem  11372  prodmodclem3  11376  prodmodclem2a  11377  zproddc  11380  fprodseq  11384  infssuzcldc  11680  iuncld  12323  fsumcncntop  12764