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  3335  elrabf  3347  sbcel12  3960  rabxfrd  4854  ffnfvf  6350  mptelixpg  7896  ac6num  9252  fproddivf  14650  fprodsplit1f  14653  ptcldmpt  21336  prdsdsf  22091  prdsxmet  22093  rmo4fOLD  29203  ssiun2sf  29241  acunirnmpt2  29320  acunirnmpt2f  29321  aciunf1lem  29322  funcnv4mpt  29331  esumc  29912  esumrnmpt2  29929  esumgect  29951  esum2dlem  29953  esum2d  29954  esumiun  29955  ldsysgenld  30022  sigapildsys  30024  fiunelros  30036  omssubadd  30161  bnj1491  30860  ptrest  33067  aomclem8  37138  ss2iundf  37459  sbcel12gOLD  38263  elunif  38685  rspcegf  38692  fiiuncl  38744  cbvmpt21  38788  eliuniincex  38804  iinssiin  38825  iinssf  38841  disjf1  38866  wessf1ornlem  38868  disjrnmpt2  38872  disjf1o  38875  disjinfi  38877  iunmapsn  38906  fmptf  38946  infnsuprnmpt  38964  iuneqfzuzlem  39037  allbutfi  39103  iooiinicc  39203  iooiinioc  39217  fsumsplit1  39231  fsumiunss  39234  fprodcnlem  39258  fprodcn  39259  climsuse  39267  climsubmpt  39319  climreclf  39323  fnlimcnv  39326  climeldmeqmpt  39327  climfveqmpt  39330  fnlimfvre  39333  fnlimabslt  39338  climfveqmpt3  39341  climbddf  39346  climeldmeqmpt3  39348  climinf2mpt  39373  climinfmpt  39374  limsupequzmptf  39390  fprodcncf  39440  dvmptmulf  39480  dvnmptdivc  39481  dvnmul  39486  dvmptfprodlem  39487  dvmptfprod  39488  dvnprodlem1  39489  dvnprodlem2  39490  stoweidlem59  39604  fourierdlem31  39683  sge00  39921  sge0f1o  39927  sge0pnffigt  39941  sge0lefi  39943  sge0resplit  39951  sge0lempt  39955  sge0iunmptlemfi  39958  sge0iunmptlemre  39960  sge0iunmpt  39963  sge0xadd  39980  sge0gtfsumgt  39988  iundjiun  40005  meadjiun  40011  meaiininclem  40028  omeiunltfirp  40061  hoidmvlelem1  40137  hoidmvlelem3  40139  hspdifhsp  40158  hoiqssbllem2  40165  hspmbllem2  40169  opnvonmbllem2  40175  hoimbl2  40207  vonhoire  40214  iinhoiicc  40216  iunhoiioo  40218  vonn0ioo2  40232  vonn0icc2  40234  incsmflem  40278  issmfle  40282  issmfgt  40293  decsmflem  40302  issmfge  40306  smflimlem2  40308  smflim  40313  smfresal  40323  smfpimbor1lem2  40334  smflim2  40340  smflimmpt  40344  smfsuplem1  40345  smfsupmpt  40349  smfsupxr  40350  smfinflem  40351  smfinfmpt  40353  smflimsuplem7  40360  smflimsuplem8  40361  smflimsup  40362  smflimsupmpt  40363  nfdfat  40535
 Copyright terms: Public domain W3C validator