Theorem nfel1 2779

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

Syntax hints:   F/wnf 1708   e. wcel 1990   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753

This theorem is referenced by:  vtocl2gf  3268  vtocl3gf  3269  vtoclgaf  3271  vtocl2gaf  3273  vtocl3gaf  3275  nfop  4418  reusv2lem4  4872  reusv2  4874  rabxfrd  4889  pofun  5051  nfse  5089  fvmptf  6301  fmptcof  6397  fliftfuns  6564  riota2f  6632  ovmpt2s  6784  ov2gf  6785  elovmpt2rab  6880  elovmpt2rab1  6881  ofmpteq  6916  fmpt2x  7236  offval22  7253  fvmpt2curryd  7397  qliftfuns  7834  xpf1o  8122  iunfi  8254  wdom2d  8485  scottex  8748  dfac8clem  8855  ac6num  9301  pwfseqlem4a  9483  pwfseqlem4  9484  gruiin  9632  rlimcld2  14309  summolem3  14445  summolem2a  14446  zsum  14449  fsum  14451  sumss2  14457  fsumcvg2  14458  fsumsplitf  14472  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fsumshftm  14513  fsum0diag2  14515  fsum00  14530  fsumabs  14533  fsumrlim  14543  fsumo1  14544  o1fsum  14545  fsumiun  14553  prodmolem3  14663  prodmolem2a  14664  zprod  14667  fprod  14671  prodss  14677  fprodser  14679  fprodm1s  14700  fprodp1s  14701  fprodabs  14704  fprodn0  14709  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  fprodsplitf  14719  fprodefsum  14825  pcmpt  15596  pcmptdvds  15598  gsumsnf  18353  gsumply1eq  19675  mdetralt2  20415  mdetunilem2  20419  fiuncmp  21207  elptr2  21377  ptcld  21416  ptcnplem  21424  ptcnp  21425  elmptrab  21630  utopsnneiplem  22051  prdsdsf  22172  prdsxmet  22174  fsumcn  22673  ovolfiniun  23269  ovoliunlem3  23272  ovoliun  23273  ovoliun2  23274  finiunmbl  23312  volfiniun  23315  iunmbl  23321  voliun  23322  itgfsum  23593  itgabs  23601  dvmptfsum  23738  dvfsumle  23784  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem3  23791  dvfsumlem4  23792  dvfsumrlim  23794  dvfsumrlim2  23795  dvfsum2  23797  itgsubst  23812  fsumdvdscom  24911  fsumvma  24938  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  fsumiunle  29575  locfinreflem  29907  esumcl  30092  esum0  30111  esumcst  30125  esumfsup  30132  esum2d  30155  measiun  30281  voliune  30292  volfiniune  30293  iota5f  31606  phpreu  33393  poimirlem25  33434  poimirlem26  33435  poimirlem28  33437  itgabsnc  33479  fsumshftd  34237  fsumshftdOLD  34238  riotasv2s  34244  cdlemefs32sn1aw  35702  mzpsubmpt  37306  mzpsubst  37311  eq0rabdioph  37340  eqrabdioph  37341  rabdiophlem2  37366  fphpd  37380  monotuz  37506  monotoddzz  37508  oddcomabszz  37509  flcidc  37744  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  rfcnnnub  39195  supxrleubrnmptf  39680  fsumclf  39801  fsummulc1f  39802  fsumnncl  39803  fsumf1of  39806  fsumreclf  39808  fsumlessf  39809  fsumsermpt  39811  fmul01  39812  fmuldfeqlem1  39814  fmuldfeq  39815  fmul01lt1lem1  39816  fmul01lt1lem2  39817  fprodexp  39826  fprodabs2  39827  fprodcnlem  39831  climmulf  39836  climsuse  39840  climrecf  39841  climaddf  39847  0ellimcdiv  39881  climsubmpt  39892  climfveqf  39912  climinf2mpt  39946  climinfmpt  39947  fprodcncf  40114  dvmptmulf  40152  iblspltprt  40189  stoweidlem3  40220  stoweidlem19  40236  stoweidlem22  40239  stoweidlem42  40259  fourierdlem31  40355  fourierdlem86  40409  fourierdlem89  40412  fourierdlem91  40414  fourierdlem112  40435  sge0f1o  40599  sge0lempt  40627  sge0iunmpt  40635  sge0ltfirpmpt2  40643  sge0isummpt2  40649  sge0xaddlem2  40651  sge0xadd  40652  vonhoire  40886  salpreimagelt  40918  smflim  40985  smfresal  40995  smfinflem  41023  eu2ndop1stv  41202