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

Theorem nfel 2763
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 2759 . 2 (⊤ → Ⅎ𝑥 𝐴𝐵)
65trud 1484 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wtru 1476  wnf 1699  wcel 1977  wnfc 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740
This theorem is referenced by:  nfel1  2765  nfel2  2767  nfnel  2890  elabgf  3317  elrabf  3329  sbcel12  3935  rabxfrd  4815  ffnfvf  6296  mptelixpg  7831  ac6num  9184  fproddivf  14557  fprodsplit1f  14560  ptcldmpt  21227  prdsdsf  21982  prdsxmet  21984  rmo4fOLD  28720  iunin1f  28757  iunxsngf  28758  ssiun2sf  28760  acunirnmpt2  28842  acunirnmpt2f  28843  aciunf1lem  28844  funcnv4mpt  28853  esumc  29440  esumrnmpt2  29457  esumgect  29479  esum2dlem  29481  esum2d  29482  esumiun  29483  ldsysgenld  29550  sigapildsys  29552  fiunelros  29564  omssubadd  29689  bnj1491  30379  ptrest  32578  aomclem8  36649  ss2iundf  36970  sbcel12gOLD  37775  elunif  38198  rspcegf  38205  iunxsngf2  38255  fiiuncl  38259  rspcef  38267  dfcleqf  38281  iunssf  38290  cbvmpt22  38305  cbvmpt21  38306  eliin2f  38316  eliuniincex  38323  disjf1  38364  wessf1ornlem  38366  disjrnmpt2  38370  disjf1o  38373  disjinfi  38375  iunmapsn  38404  iuneqfzuzlem  38491  allbutfi  38557  iooiinicc  38616  iooiinioc  38630  fsumsplit1  38639  fsumiunss  38642  fprodcnlem  38666  fprodcn  38667  climsuse  38675  climsubmpt  38727  climreclf  38731  fnlimcnv  38734  climeldmeqmpt  38735  climfveqmpt  38738  fnlimfvre  38741  fnlimabslt  38746  fprodcncf  38787  dvmptmulf  38827  dvnmptdivc  38828  dvnmul  38833  dvmptfprodlem  38834  dvmptfprod  38835  dvnprodlem1  38836  dvnprodlem2  38837  stoweidlem59  38952  fourierdlem31  39031  sge00  39269  sge0f1o  39275  sge0pnffigt  39289  sge0lefi  39291  sge0resplit  39299  sge0lempt  39303  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0xadd  39328  sge0gtfsumgt  39336  iundjiun  39353  meadjiun  39359  meaiininclem  39376  omeiunltfirp  39409  hoidmvlelem1  39485  hoidmvlelem3  39487  hspdifhsp  39506  hoiqssbllem2  39513  hspmbllem2  39517  opnvonmbllem2  39523  hoimbl2  39555  vonhoire  39563  iinhoiicc  39565  iunhoiioo  39567  vonn0ioo2  39581  vonn0icc2  39583  incsmflem  39628  issmfle  39632  issmfgt  39643  decsmflem  39652  issmfge  39656  smflimlem2  39658  smflim  39663  smfresal  39673  smfpimbor1lem2  39684  nfdfat  39859
  Copyright terms: Public domain W3C validator