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

Theorem nfel 2926
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 2922 . 2 (⊤ → Ⅎ𝑥 𝐴𝐵)
65trud 1641 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1632  wnf 1856  wcel 2145  wnfc 2900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-clel 2767  df-nfc 2902
This theorem is referenced by:  nfel1  2928  nfel2  2930  nfnel  3053  elabgf  3499  elrabf  3511  sbcel12  4127  rabxfrd  5017  ffnfvf  6531  mptelixpg  8099  ac6num  9503  fproddivf  14924  fprodsplit1f  14927  ptcldmpt  21638  prdsdsf  22392  prdsxmet  22394  rmo4fOLD  29675  ssiun2sf  29716  acunirnmpt2  29800  acunirnmpt2f  29801  aciunf1lem  29802  funcnv4mpt  29810  fsumiunle  29915  esumc  30453  esumrnmpt2  30470  esumgect  30492  esum2dlem  30494  esum2d  30495  esumiun  30496  ldsysgenld  30563  sigapildsys  30565  fiunelros  30577  omssubadd  30702  breprexplema  31048  bnj1491  31463  ptrest  33741  aomclem8  38157  ss2iundf  38477  sbcel12gOLD  39279  elunif  39697  rspcegf  39704  fiiuncl  39755  cbvmpt21  39799  eliuniincex  39813  iinssiin  39833  iinssf  39848  disjf1  39889  wessf1ornlem  39891  disjrnmpt2  39895  disjf1o  39898  disjinfi  39900  iunmapsn  39927  fmptf  39966  infnsuprnmpt  39983  iuneqfzuzlem  40066  allbutfi  40132  supminfrnmpt  40188  supminfxrrnmpt  40217  monoordxr  40229  monoord2xr  40231  iooiinicc  40287  iooiinioc  40301  fsumsplit1  40322  fsumiunss  40325  fprodcnlem  40349  fprodcn  40350  climsuse  40358  climsubmpt  40410  climreclf  40414  fnlimcnv  40417  climeldmeqmpt  40418  climfveqmpt  40421  fnlimfvre  40424  fnlimabslt  40429  climfveqmpt3  40432  climbddf  40437  climeldmeqmpt3  40439  climinf2mpt  40464  climinfmpt  40465  limsupequzmptf  40481  lmbr3  40497  fprodcncf  40632  dvmptmulf  40670  dvnmptdivc  40671  dvnmul  40676  dvmptfprodlem  40677  dvmptfprod  40678  dvnprodlem1  40679  dvnprodlem2  40680  stoweidlem59  40793  fourierdlem31  40872  sge00  41110  sge0f1o  41116  sge0pnffigt  41130  sge0lefi  41132  sge0resplit  41140  sge0lempt  41144  sge0iunmptlemfi  41147  sge0iunmptlemre  41149  sge0iunmpt  41152  sge0xadd  41169  sge0gtfsumgt  41177  iundjiun  41194  meadjiun  41200  meaiininclem  41220  omeiunltfirp  41253  hoidmvlelem1  41329  hoidmvlelem3  41331  hspdifhsp  41350  hoiqssbllem2  41357  hspmbllem2  41361  opnvonmbllem2  41367  hoimbl2  41399  vonhoire  41406  iinhoiicc  41408  iunhoiioo  41410  vonn0ioo2  41424  vonn0icc2  41426  incsmflem  41470  issmfle  41474  issmfgt  41485  decsmflem  41494  issmfge  41498  smflimlem2  41500  smflim  41505  smfresal  41515  smfpimbor1lem2  41526  smflim2  41532  smflimmpt  41536  smfsuplem1  41537  smfsupmpt  41541  smfsupxr  41542  smfinflem  41543  smfinfmpt  41545  smflimsuplem7  41552  smflimsuplem8  41553  smflimsup  41554  smflimsupmpt  41555  smfliminf  41557  smfliminfmpt  41558  nfdfat  41730
  Copyright terms: Public domain W3C validator