MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfel1 Structured version   Visualization version   GIF version

Theorem nfel1 2776
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
StepHypRef Expression
1 nfeq1.1 . 2 𝑥𝐴
2 nfcv 2762 . 2 𝑥𝐵
31, 2nfel 2774 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1706  wcel 1988  wnfc 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-cleq 2613  df-clel 2616  df-nfc 2751
This theorem is referenced by:  vtocl2gf  3263  vtocl3gf  3264  vtoclgaf  3266  vtocl2gaf  3268  vtocl3gaf  3270  nfop  4409  reusv2lem4  4863  reusv2  4865  rabxfrd  4880  pofun  5041  nfse  5079  fvmptf  6287  fmptcof  6383  fliftfuns  6549  riota2f  6617  ovmpt2s  6769  ov2gf  6770  elovmpt2rab  6865  elovmpt2rab1  6866  ofmpteq  6901  fmpt2x  7221  offval22  7238  fvmpt2curryd  7382  qliftfuns  7819  xpf1o  8107  iunfi  8239  wdom2d  8470  scottex  8733  dfac8clem  8840  ac6num  9286  pwfseqlem4a  9468  pwfseqlem4  9469  gruiin  9617  rlimcld2  14290  summolem3  14426  summolem2a  14427  zsum  14430  fsum  14432  sumss2  14438  fsumcvg2  14439  fsumsplitf  14453  fsum2dlem  14482  fsumcom2  14486  fsumcom2OLD  14487  fsumshftm  14494  fsum0diag2  14496  fsum00  14511  fsumabs  14514  fsumrlim  14524  fsumo1  14525  o1fsum  14526  fsumiun  14534  prodmolem3  14644  prodmolem2a  14645  zprod  14648  fprod  14652  prodss  14658  fprodser  14660  fprodm1s  14681  fprodp1s  14682  fprodabs  14685  fprodn0  14690  fprod2dlem  14691  fprodcom2  14695  fprodcom2OLD  14696  fprodsplitf  14700  fprodefsum  14806  pcmpt  15577  pcmptdvds  15579  gsumsnf  18334  gsumply1eq  19656  mdetralt2  20396  mdetunilem2  20400  fiuncmp  21188  elptr2  21358  ptcld  21397  ptcnplem  21405  ptcnp  21406  elmptrab  21611  utopsnneiplem  22032  prdsdsf  22153  prdsxmet  22155  fsumcn  22654  ovolfiniun  23250  ovoliunlem3  23253  ovoliun  23254  ovoliun2  23255  finiunmbl  23293  volfiniun  23296  iunmbl  23302  voliun  23303  itgfsum  23574  itgabs  23582  dvmptfsum  23719  dvfsumle  23765  dvfsumabs  23767  dvfsumlem1  23770  dvfsumlem3  23772  dvfsumlem4  23773  dvfsumrlim  23775  dvfsumrlim2  23776  dvfsum2  23778  itgsubst  23793  fsumdvdscom  24892  fsumvma  24919  dchrisumlema  25158  dchrisumlem2  25160  dchrisumlem3  25161  fsumiunle  29549  locfinreflem  29881  esumcl  30066  esum0  30085  esumcst  30099  esumfsup  30106  esum2d  30129  measiun  30255  voliune  30266  volfiniune  30267  iota5f  31581  phpreu  33364  poimirlem25  33405  poimirlem26  33406  poimirlem28  33408  itgabsnc  33450  fsumshftd  34056  fsumshftdOLD  34057  riotasv2s  34063  cdlemefs32sn1aw  35521  mzpsubmpt  37125  mzpsubst  37130  eq0rabdioph  37159  eqrabdioph  37160  rabdiophlem2  37185  fphpd  37199  monotuz  37325  monotoddzz  37327  oddcomabszz  37328  flcidc  37563  binomcxplemdvbinom  38372  binomcxplemdvsum  38374  binomcxplemnotnn0  38375  rfcnnnub  39015  supxrleubrnmptf  39493  fsumclf  39601  fsummulc1f  39602  fsumnncl  39603  fsumf1of  39606  fsumreclf  39608  fsumlessf  39609  fsumsermpt  39611  fmul01  39612  fmuldfeqlem1  39614  fmuldfeq  39615  fmul01lt1lem1  39616  fmul01lt1lem2  39617  fprodexp  39626  fprodabs2  39627  fprodcnlem  39631  climmulf  39636  climsuse  39640  climrecf  39641  climaddf  39647  0ellimcdiv  39681  climsubmpt  39692  climfveqf  39712  climinf2mpt  39746  climinfmpt  39747  fprodcncf  39877  dvmptmulf  39915  iblspltprt  39952  stoweidlem3  39983  stoweidlem19  39999  stoweidlem22  40002  stoweidlem42  40022  fourierdlem31  40118  fourierdlem86  40172  fourierdlem89  40175  fourierdlem91  40177  fourierdlem112  40198  sge0f1o  40362  sge0lempt  40390  sge0iunmpt  40398  sge0ltfirpmpt2  40406  sge0isummpt2  40412  sge0xaddlem2  40414  sge0xadd  40415  vonhoire  40649  salpreimagelt  40681  smflim  40748  smfresal  40758  smfinflem  40786  eu2ndop1stv  40965
  Copyright terms: Public domain W3C validator