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

Theorem nfel 2915
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 2911 . 2 (⊤ → Ⅎ𝑥 𝐴𝐵)
65trud 1642 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1633  wnf 1857  wcel 2139  wnfc 2889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-cleq 2753  df-clel 2756  df-nfc 2891
This theorem is referenced by:  nfel1  2917  nfel2  2919  nfnel  3042  elabgf  3488  elrabf  3500  sbcel12  4126  rabxfrd  5038  ffnfvf  6552  mptelixpg  8111  ac6num  9493  fproddivf  14917  fprodsplit1f  14920  ptcldmpt  21619  prdsdsf  22373  prdsxmet  22375  rmo4fOLD  29644  ssiun2sf  29685  acunirnmpt2  29769  acunirnmpt2f  29770  aciunf1lem  29771  funcnv4mpt  29779  fsumiunle  29884  esumc  30422  esumrnmpt2  30439  esumgect  30461  esum2dlem  30463  esum2d  30464  esumiun  30465  ldsysgenld  30532  sigapildsys  30534  fiunelros  30546  omssubadd  30671  breprexplema  31017  bnj1491  31432  ptrest  33721  aomclem8  38133  ss2iundf  38453  sbcel12gOLD  39256  elunif  39674  rspcegf  39681  fiiuncl  39733  cbvmpt21  39777  eliuniincex  39791  iinssiin  39811  iinssf  39826  disjf1  39868  wessf1ornlem  39870  disjrnmpt2  39874  disjf1o  39877  disjinfi  39879  iunmapsn  39908  fmptf  39947  infnsuprnmpt  39964  iuneqfzuzlem  40048  allbutfi  40114  supminfrnmpt  40170  supminfxrrnmpt  40199  monoordxr  40211  monoord2xr  40213  iooiinicc  40272  iooiinioc  40286  fsumsplit1  40307  fsumiunss  40310  fprodcnlem  40334  fprodcn  40335  climsuse  40343  climsubmpt  40395  climreclf  40399  fnlimcnv  40402  climeldmeqmpt  40403  climfveqmpt  40406  fnlimfvre  40409  fnlimabslt  40414  climfveqmpt3  40417  climbddf  40422  climeldmeqmpt3  40424  climinf2mpt  40449  climinfmpt  40450  limsupequzmptf  40466  lmbr3  40482  fprodcncf  40617  dvmptmulf  40655  dvnmptdivc  40656  dvnmul  40661  dvmptfprodlem  40662  dvmptfprod  40663  dvnprodlem1  40664  dvnprodlem2  40665  stoweidlem59  40779  fourierdlem31  40858  sge00  41096  sge0f1o  41102  sge0pnffigt  41116  sge0lefi  41118  sge0resplit  41126  sge0lempt  41130  sge0iunmptlemfi  41133  sge0iunmptlemre  41135  sge0iunmpt  41138  sge0xadd  41155  sge0gtfsumgt  41163  iundjiun  41180  meadjiun  41186  meaiininclem  41206  omeiunltfirp  41239  hoidmvlelem1  41315  hoidmvlelem3  41317  hspdifhsp  41336  hoiqssbllem2  41343  hspmbllem2  41347  opnvonmbllem2  41353  hoimbl2  41385  vonhoire  41392  iinhoiicc  41394  iunhoiioo  41396  vonn0ioo2  41410  vonn0icc2  41412  incsmflem  41456  issmfle  41460  issmfgt  41471  decsmflem  41480  issmfge  41484  smflimlem2  41486  smflim  41491  smfresal  41501  smfpimbor1lem2  41512  smflim2  41518  smflimmpt  41522  smfsuplem1  41523  smfsupmpt  41527  smfsupxr  41528  smfinflem  41529  smfinfmpt  41531  smflimsuplem7  41538  smflimsuplem8  41539  smflimsup  41540  smflimsupmpt  41541  smfliminf  41543  smfliminfmpt  41544  nfdfat  41716
  Copyright terms: Public domain W3C validator