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

Theorem nfel 2773
Description: Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
Hypotheses
Ref Expression
nfnfc.1 𝑥𝐴
nfeq.2 𝑥𝐵
Assertion
Ref Expression
nfel 𝑥 𝐴𝐵

Proof of Theorem nfel
StepHypRef Expression
1 nfnfc.1 . . . 4 𝑥𝐴
21a1i 11 . . 3 (⊤ → 𝑥𝐴)
3 nfeq.2 . . . 4 𝑥𝐵
43a1i 11 . . 3 (⊤ → 𝑥𝐵)
52, 4nfeld 2769 . 2 (⊤ → Ⅎ𝑥 𝐴𝐵)
65trud 1490 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1481  wnf 1705  wcel 1987  wnfc 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-clel 2617  df-nfc 2750
This theorem is referenced by:  nfel1  2775  nfel2  2777  nfnel  2900  elabgf  3336  elrabf  3348  sbcel12  3961  rabxfrd  4859  ffnfvf  6355  mptelixpg  7905  ac6num  9261  fproddivf  14662  fprodsplit1f  14665  ptcldmpt  21357  prdsdsf  22112  prdsxmet  22114  rmo4fOLD  29225  ssiun2sf  29264  acunirnmpt2  29343  acunirnmpt2f  29344  aciunf1lem  29345  funcnv4mpt  29354  esumc  29936  esumrnmpt2  29953  esumgect  29975  esum2dlem  29977  esum2d  29978  esumiun  29979  ldsysgenld  30046  sigapildsys  30048  fiunelros  30060  omssubadd  30185  bnj1491  30886  ptrest  33079  aomclem8  37150  ss2iundf  37471  sbcel12gOLD  38275  elunif  38697  rspcegf  38704  fiiuncl  38756  cbvmpt21  38800  eliuniincex  38816  iinssiin  38837  iinssf  38853  disjf1  38878  wessf1ornlem  38880  disjrnmpt2  38884  disjf1o  38887  disjinfi  38889  iunmapsn  38918  fmptf  38958  infnsuprnmpt  38976  iuneqfzuzlem  39049  allbutfi  39115  iooiinicc  39215  iooiinioc  39229  fsumsplit1  39240  fsumiunss  39243  fprodcnlem  39267  fprodcn  39268  climsuse  39276  climsubmpt  39328  climreclf  39332  fnlimcnv  39335  climeldmeqmpt  39336  climfveqmpt  39339  fnlimfvre  39342  fnlimabslt  39347  climfveqmpt3  39350  climbddf  39355  climeldmeqmpt3  39357  climinf2mpt  39382  climinfmpt  39383  limsupequzmptf  39399  fprodcncf  39449  dvmptmulf  39489  dvnmptdivc  39490  dvnmul  39495  dvmptfprodlem  39496  dvmptfprod  39497  dvnprodlem1  39498  dvnprodlem2  39499  stoweidlem59  39613  fourierdlem31  39692  sge00  39930  sge0f1o  39936  sge0pnffigt  39950  sge0lefi  39952  sge0resplit  39960  sge0lempt  39964  sge0iunmptlemfi  39967  sge0iunmptlemre  39969  sge0iunmpt  39972  sge0xadd  39989  sge0gtfsumgt  39997  iundjiun  40014  meadjiun  40020  meaiininclem  40037  omeiunltfirp  40070  hoidmvlelem1  40146  hoidmvlelem3  40148  hspdifhsp  40167  hoiqssbllem2  40174  hspmbllem2  40178  opnvonmbllem2  40184  hoimbl2  40216  vonhoire  40223  iinhoiicc  40225  iunhoiioo  40227  vonn0ioo2  40241  vonn0icc2  40243  incsmflem  40287  issmfle  40291  issmfgt  40302  decsmflem  40311  issmfge  40315  smflimlem2  40317  smflim  40322  smfresal  40332  smfpimbor1lem2  40343  smflim2  40349  smflimmpt  40353  smfsuplem1  40354  smfsupmpt  40358  smfsupxr  40359  smfinflem  40360  smfinfmpt  40362  smflimsuplem7  40369  smflimsuplem8  40370  smflimsup  40371  smflimsupmpt  40372  nfdfat  40544
  Copyright terms: Public domain W3C validator