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

Theorem nfel1 2764
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 2750 . 2 𝑥𝐵
31, 2nfel 2762 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1698  wcel 1976  wnfc 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-nfc 2739
This theorem is referenced by:  vtocl2gf  3240  vtocl3gf  3241  vtoclgaf  3243  vtocl2gaf  3245  vtocl3gaf  3247  nfop  4350  reusv2lem4  4793  reusv2  4795  rabxfrd  4810  pofun  4965  nfse  5003  fvmptf  6194  fmptcof  6289  fliftfuns  6442  riota2f  6510  ovmpt2s  6660  ov2gf  6661  elovmpt2rab  6755  elovmpt2rab1  6756  ofmpteq  6791  fmpt2x  7102  offval22  7117  fvmpt2curryd  7261  qliftfuns  7698  xpf1o  7984  iunfi  8114  wdom2d  8345  scottex  8608  dfac8clem  8715  ac6num  9161  pwfseqlem4a  9339  pwfseqlem4  9340  gruiin  9488  rlimcld2  14103  summolem3  14238  summolem2a  14239  zsum  14242  fsum  14244  sumss2  14250  fsumcvg2  14251  fsum2dlem  14289  fsumcom2  14293  fsumcom2OLD  14294  fsumshftm  14301  fsum0diag2  14303  fsum00  14317  fsumabs  14320  fsumrlim  14330  fsumo1  14331  o1fsum  14332  fsumiun  14340  prodmolem3  14448  prodmolem2a  14449  zprod  14452  fprod  14456  prodss  14462  fprodser  14464  fprodm1s  14485  fprodp1s  14486  fprodabs  14489  fprodn0  14494  fprod2dlem  14495  fprodcom2  14499  fprodcom2OLD  14500  fprodsplitf  14504  fprodefsum  14610  pcmpt  15380  pcmptdvds  15382  gsumsnf  18122  gsumply1eq  19442  mdetralt2  20176  mdetunilem2  20180  fiuncmp  20959  elptr2  21129  ptcld  21168  ptcnplem  21176  ptcnp  21177  elmptrab  21382  utopsnneiplem  21803  prdsdsf  21923  prdsxmet  21925  fsumcn  22412  ovolfiniun  22993  ovoliunlem3  22996  ovoliun  22997  ovoliun2  22998  finiunmbl  23036  volfiniun  23039  iunmbl  23045  voliun  23046  itgfsum  23316  itgabs  23324  dvmptfsum  23459  dvfsumle  23505  dvfsumabs  23507  dvfsumlem1  23510  dvfsumlem3  23512  dvfsumlem4  23513  dvfsumrlim  23515  dvfsumrlim2  23516  dvfsum2  23518  itgsubst  23533  fsumdvdscom  24628  fsumvma  24655  dchrisumlema  24894  dchrisumlem2  24896  dchrisumlem3  24897  locfinreflem  29041  esumcl  29225  esum0  29244  esumcst  29258  esumfsup  29265  esum2d  29288  measiun  29414  voliune  29425  volfiniune  29426  iota5f  30667  phpreu  32366  poimirlem25  32407  poimirlem26  32408  poimirlem28  32410  itgabsnc  32452  fsumshftd  33058  fsumshftdOLD  33059  riotasv2s  33065  cdlemefs32sn1aw  34523  mzpsubmpt  36127  mzpsubst  36132  eq0rabdioph  36161  eqrabdioph  36162  rabdiophlem2  36187  fphpd  36201  monotuz  36327  monotoddzz  36329  oddcomabszz  36330  flcidc  36566  binomcxplemdvbinom  37377  binomcxplemdvsum  37379  binomcxplemnotnn0  37380  rfcnnnub  38021  fsumclf  38437  fsumsplitf  38438  fsummulc1f  38439  fsumnncl  38442  fsumf1of  38445  fsumreclf  38447  fsumlessf  38448  fsumsermpt  38450  fmul01  38451  fmuldfeqlem1  38453  fmuldfeq  38454  fmul01lt1lem1  38455  fmul01lt1lem2  38456  fprodexp  38465  fprodabs2  38466  fprodcnlem  38470  climmulf  38475  climsuse  38479  climrecf  38480  climaddf  38486  0ellimcdiv  38520  climsubmpt  38531  fprodcncf  38591  dvmptmulf  38631  iblspltprt  38669  stoweidlem3  38700  stoweidlem19  38716  stoweidlem22  38719  stoweidlem42  38739  fourierdlem31  38835  fourierdlem86  38889  fourierdlem89  38892  fourierdlem91  38894  fourierdlem112  38915  sge0f1o  39079  sge0lempt  39107  sge0iunmpt  39115  sge0ltfirpmpt2  39123  sge0isummpt2  39129  sge0xaddlem2  39131  sge0xadd  39132  vonhoire  39367  salpreimagelt  39399  smflim  39467  smfresal  39477  eu2ndop1stv  39655
  Copyright terms: Public domain W3C validator