Theorem nfel1 2911

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 2894	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2909	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2111  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2723  df-clel 2806  df-nfc 2881

This theorem is referenced by:  vtocl2gf  3523  vtocl3gf  3524  vtoclgaf  3527  vtocl2gaf  3530  vtocl2gafOLD  3531  vtocl3gaf  3532  vtocl3gafOLD  3533  nfop  4838  reusv2lem4  5337  reusv2  5339  rabxfrd  5353  pofun  5540  nfse  5588  fvmptf  6950  fmptcof  7063  fliftfuns  7248  riota2f  7327  ovmpos  7494  ov2gf  7495  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  ofmpteq  7633  fmpox  7999  offval22  8018  fvmpocurryd  8201  qliftfuns  8728  xpf1o  9052  iunfi  9227  wdom2d  9466  scottex  9778  dfac8clem  9923  ac6num  10370  pwfseqlem4a  10552  pwfseqlem4  10553  gruiin  10701  rlimcld2  15485  summolem3  15621  summolem2a  15622  zsum  15625  fsum  15627  sumss2  15633  fsumcvg2  15634  fsumclf  15645  fsumsplitf  15649  fsum2dlem  15677  fsumcom2  15681  fsumshftm  15688  fsum0diag2  15690  fsum00  15705  fsumabs  15708  fsumrlim  15718  fsumo1  15719  o1fsum  15720  fsumiun  15728  prodmolem3  15840  prodmolem2a  15841  zprod  15844  fprod  15848  prodss  15854  fprodser  15856  fprodm1s  15877  fprodp1s  15878  fprodabs  15881  fprodn0  15886  fprod2dlem  15887  fprodcom2  15891  fproddivf  15894  fprodsplitf  15895  fprodsplit1f  15897  fprodefsum  16002  pcmpt  16804  pcmptdvds  16806  gsumsnf  19865  gsumply1eq  22224  mdetralt2  22524  mdetunilem2  22528  fiuncmp  23319  elptr2  23489  ptcld  23528  ptcnplem  23536  ptcnp  23537  elmptrab  23742  utopsnneiplem  24162  prdsdsf  24282  prdsxmet  24284  fsumcn  24788  ovolfiniun  25429  ovoliunlem3  25432  ovoliun  25433  ovoliun2  25434  finiunmbl  25472  volfiniun  25475  iunmbl  25481  voliun  25482  itgfsum  25755  itgabs  25763  dvmptfsum  25906  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem1  25959  dvfsumlem3  25962  dvfsumlem4  25963  dvfsumrlim  25965  dvfsumrlim2  25966  dvfsum2  25968  itgsubst  25983  fsumdvdscom  27122  fsumvma  27151  dchrisumlema  27426  dchrisumlem2  27428  dchrisumlem3  27429  fsumiunle  32812  locfinreflem  33853  esumcl  34043  esum0  34062  esumcst  34076  esumfsup  34083  esum2d  34106  measiun  34231  voliune  34242  volfiniune  34243  iota5f  35768  weiunse  36512  phpreu  37654  poimirlem25  37695  poimirlem26  37696  poimirlem28  37698  itgabsnc  37739  fsumshftd  39061  riotasv2s  39067  cdlemefs32sn1aw  40523  mzpsubmpt  42846  mzpsubst  42851  eq0rabdioph  42879  eqrabdioph  42880  rabdiophlem2  42905  fphpd  42919  monotuz  43044  monotoddzz  43046  oddcomabszz  43047  flcidc  43273  binomcxplemdvbinom  44456  binomcxplemdvsum  44458  binomcxplemnotnn0  44459  modelaxreplem3  45083  rfcnnnub  45143  disjinfi  45299  supxrleubrnmptf  45559  caucvgbf  45597  cvgcaule  45599  fsummulc1f  45681  fsumnncl  45682  fsumf1of  45684  fsumreclf  45686  fsumlessf  45687  fsumsermpt  45689  fmul01  45690  fmuldfeqlem1  45692  fmuldfeq  45693  fmul01lt1lem1  45694  fmul01lt1lem2  45695  fprodexp  45704  fprodabs2  45705  fprodcnlem  45709  climmulf  45714  climsuse  45718  climrecf  45719  climaddf  45725  0ellimcdiv  45757  climsubmpt  45768  climfveqf  45788  climinf2mpt  45822  climinfmpt  45823  fprodcncf  46008  dvmptmulf  46045  dvmptfprod  46053  iblspltprt  46081  stoweidlem3  46111  stoweidlem19  46127  stoweidlem22  46130  stoweidlem42  46150  fourierdlem31  46246  fourierdlem86  46300  fourierdlem89  46303  fourierdlem91  46305  fourierdlem112  46326  sge0f1o  46490  sge0lempt  46518  sge0iunmpt  46526  sge0ltfirpmpt2  46534  sge0isummpt2  46540  sge0xaddlem2  46542  sge0xadd  46543  vonhoire  46780  salpreimagelt  46815  smflim  46885  smfresal  46896  smfinflem  46925  eu2ndop1stv  47235