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

Theorem nfel 2922
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 2919 . 2 (⊤ → Ⅎ𝑥 𝐴𝐵)
65mptru 1549 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1543  wnf 1786  wcel 2107  wnfc 2888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2729  df-clel 2815  df-nfc 2890
This theorem is referenced by:  nfel1  2924  nfel2  2926  nfnel  3057  elabgf  3631  elrabf  3646  sbcel12  4373  rabxfrd  5377  ffnfvf  7072  nfixpw  8861  mptelixpg  8880  fsumsplit1  15637  ptcldmpt  22981  prdsdsf  23736  prdsxmet  23738  ssiun2sf  31520  iinabrex  31529  acunirnmpt2  31618  acunirnmpt2f  31619  aciunf1lem  31620  funcnv4mpt  31627  fsumiunle  31767  zarclsiin  32492  esumc  32690  esumrnmpt2  32707  esumgect  32729  esum2dlem  32731  esum2d  32732  esumiun  32733  ldsysgenld  32799  sigapildsys  32801  fiunelros  32813  omssubadd  32940  breprexplema  33283  bnj1491  33709  currysetlem  35445  currysetlem1  35447  ptrest  36106  aomclem8  41417  ss2iundf  42005  elunif  43295  rspcegf  43302  fiiuncl  43347  eliuniincex  43393  disjf1  43475  disjf1o  43484  iunmapsn  43512  fmptf  43539  infnsuprnmpt  43552  fmptff  43572  iuneqfzuzlem  43642  allbutfi  43702  supminfrnmpt  43754  supminfxrrnmpt  43780  monoordxr  43792  monoord2xr  43794  iooiinicc  43854  iooiinioc  43868  fsumiunss  43890  fprodcnlem  43914  fprodcn  43915  climsuse  43923  climsubmpt  43975  climreclf  43979  fnlimcnv  43982  climeldmeqmpt  43983  climfveqmpt  43986  fnlimfvre  43989  fnlimabslt  43994  climfveqmpt3  43997  climbddf  44002  climeldmeqmpt3  44004  climinf2mpt  44029  climinfmpt  44030  limsupequzmptf  44046  lmbr3  44062  fprodcncf  44215  dvmptmulf  44252  dvnmptdivc  44253  dvnmul  44258  dvmptfprodlem  44259  dvmptfprod  44260  dvnprodlem1  44261  dvnprodlem2  44262  stoweidlem59  44374  fourierdlem31  44453  sge00  44691  sge0f1o  44697  sge0pnffigt  44711  sge0lefi  44713  sge0resplit  44721  sge0lempt  44725  sge0iunmptlemfi  44728  sge0iunmptlemre  44730  sge0iunmpt  44733  sge0xadd  44750  sge0gtfsumgt  44758  iundjiun  44775  meadjiun  44781  meaiininclem  44801  omeiunltfirp  44834  hoidmvlelem1  44910  hoidmvlelem3  44912  hspdifhsp  44931  hoiqssbllem2  44938  hspmbllem2  44942  opnvonmbllem2  44948  hoimbl2  44980  vonhoire  44987  iinhoiicc  44989  iunhoiioo  44991  vonn0ioo2  45005  vonn0icc2  45007  incsmflem  45056  issmfle  45060  issmfgt  45071  decsmflem  45081  issmfge  45085  smflimlem2  45087  smflim  45092  smfresal  45103  smfpimbor1lem2  45114  smflim2  45121  smflimmpt  45125  smfsuplem1  45126  smfsupxr  45131  smfinflem  45132  smfinfmpt  45134  smflimsuplem7  45141  smflimsuplem8  45142  smflimsup  45143  smflimsupmpt  45144  smfliminf  45146  smfliminfmpt  45147  nfdfat  45433
  Copyright terms: Public domain W3C validator