Theorem nfel1 2925

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

Syntax hints:  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-cleq 2732  df-clel 2819  df-nfc 2895

This theorem is referenced by:  vtocl2gf  3584  vtocl3gf  3585  vtoclgaf  3588  vtocl2gaf  3591  vtocl2gafOLD  3592  vtocl3gaf  3593  vtocl3gafOLD  3594  nfop  4913  reusv2lem4  5419  reusv2  5421  rabxfrd  5435  pofun  5626  nfse  5674  fvmptf  7050  fmptcof  7164  fliftfuns  7350  riota2f  7429  ovmpos  7598  ov2gf  7599  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  ofmpteq  7736  fmpox  8108  offval22  8129  fvmpocurryd  8312  qliftfuns  8862  xpf1o  9205  iunfi  9411  wdom2d  9649  scottex  9954  dfac8clem  10101  ac6num  10548  pwfseqlem4a  10730  pwfseqlem4  10731  gruiin  10879  rlimcld2  15624  summolem3  15762  summolem2a  15763  zsum  15766  fsum  15768  sumss2  15774  fsumcvg2  15775  fsumclf  15786  fsumsplitf  15790  fsum2dlem  15818  fsumcom2  15822  fsumshftm  15829  fsum0diag2  15831  fsum00  15846  fsumabs  15849  fsumrlim  15859  fsumo1  15860  o1fsum  15861  fsumiun  15869  prodmolem3  15981  prodmolem2a  15982  zprod  15985  fprod  15989  prodss  15995  fprodser  15997  fprodm1s  16018  fprodp1s  16019  fprodabs  16022  fprodn0  16027  fprod2dlem  16028  fprodcom2  16032  fproddivf  16035  fprodsplitf  16036  fprodsplit1f  16038  fprodefsum  16143  pcmpt  16939  pcmptdvds  16941  gsumsnf  19995  gsumply1eq  22334  mdetralt2  22636  mdetunilem2  22640  fiuncmp  23433  elptr2  23603  ptcld  23642  ptcnplem  23650  ptcnp  23651  elmptrab  23856  utopsnneiplem  24277  prdsdsf  24398  prdsxmet  24400  fsumcn  24913  ovolfiniun  25555  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  finiunmbl  25598  volfiniun  25601  iunmbl  25607  voliun  25608  itgfsum  25882  itgabs  25890  dvmptfsum  26033  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem1  26086  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlim  26092  dvfsumrlim2  26093  dvfsum2  26095  itgsubst  26110  fsumdvdscom  27246  fsumvma  27275  dchrisumlema  27550  dchrisumlem2  27552  dchrisumlem3  27553  fsumiunle  32833  locfinreflem  33786  esumcl  33994  esum0  34013  esumcst  34027  esumfsup  34034  esum2d  34057  measiun  34182  voliune  34193  volfiniune  34194  iota5f  35686  weiunse  36434  phpreu  37564  poimirlem25  37605  poimirlem26  37606  poimirlem28  37608  itgabsnc  37649  fsumshftd  38908  riotasv2s  38914  cdlemefs32sn1aw  40371  mzpsubmpt  42699  mzpsubst  42704  eq0rabdioph  42732  eqrabdioph  42733  rabdiophlem2  42758  fphpd  42772  monotuz  42898  monotoddzz  42900  oddcomabszz  42901  flcidc  43131  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  rfcnnnub  44936  disjinfi  45099  supxrleubrnmptf  45366  caucvgbf  45405  cvgcaule  45407  fsummulc1f  45492  fsumnncl  45493  fsumf1of  45495  fsumreclf  45497  fsumlessf  45498  fsumsermpt  45500  fmul01  45501  fmuldfeqlem1  45503  fmuldfeq  45504  fmul01lt1lem1  45505  fmul01lt1lem2  45506  fprodexp  45515  fprodabs2  45516  fprodcnlem  45520  climmulf  45525  climsuse  45529  climrecf  45530  climaddf  45536  0ellimcdiv  45570  climsubmpt  45581  climfveqf  45601  climinf2mpt  45635  climinfmpt  45636  fprodcncf  45821  dvmptmulf  45858  iblspltprt  45894  stoweidlem3  45924  stoweidlem19  45940  stoweidlem22  45943  stoweidlem42  45963  fourierdlem31  46059  fourierdlem86  46113  fourierdlem89  46116  fourierdlem91  46118  fourierdlem112  46139  sge0f1o  46303  sge0lempt  46331  sge0iunmpt  46339  sge0ltfirpmpt2  46347  sge0isummpt2  46353  sge0xaddlem2  46355  sge0xadd  46356  vonhoire  46593  salpreimagelt  46628  smflim  46698  smfresal  46709  smfinflem  46738  eu2ndop1stv  47040