Theorem nfel 2937

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

Step	Hyp	Ref	Expression
1		nfnfc.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfeq.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
5	2, 4	nfeld 2934	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 ∈ 𝐵)
6	5	mptru 1566	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  ⊤wtru 1560  Ⅎwnf 1802   ∈ wcel 2141  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-cleq 2753  df-clel 2836  df-nfc 2910

This theorem is referenced by:  nfel1  2939  nfel2  2941  nfnel  3068  elabgf  3632  elrabf  3646  sbcel12  4362  rabxfrd  5371  ffnfvf  7096  nfixpw  8892  mptelixpg  8911  fsumsplit1  15763  ptcldmpt  23662  prdsdsf  24415  prdsxmet  24417  ssiun2sf  32719  iinabrex  32729  acunirnmpt2  32823  acunirnmpt2f  32824  aciunf1lem  32825  funcnv4mpt  32831  fsumiunle  32992  zarclsiin  34129  esumc  34309  esumrnmpt2  34326  esumgect  34348  esum2dlem  34350  esum2d  34351  esumiun  34352  ldsysgenld  34418  sigapildsys  34420  fiunelros  34432  omssubadd  34558  breprexplema  34885  bnj1491  35313  currysetlem  37391  currysetlem1  37393  ptrest  38079  aomclem8  43599  ss2iundf  44196  elunif  45557  rspcegf  45564  fiiuncl  45606  eliuniincex  45648  disjf1  45722  disjf1o  45730  iunmapsn  45754  fmptf  45775  infnsuprnmpt  45786  fmptff  45805  iuneqfzuzlem  45871  allbutfi  45929  supminfrnmpt  45980  supminfxrrnmpt  46006  monoordxr  46017  monoord2xr  46019  iooiinicc  46079  iooiinioc  46093  fsumiunss  46112  fprodcn  46137  climsuse  46145  climsubmpt  46195  climreclf  46199  fnlimcnv  46202  climeldmeqmpt  46203  climfveqmpt  46206  fnlimfvre  46209  fnlimabslt  46214  climfveqmpt3  46217  climbddf  46222  climeldmeqmpt3  46224  climinf2mpt  46249  climinfmpt  46250  limsupequzmptf  46266  lmbr3  46282  fprodcncf  46435  dvmptmulf  46472  dvnmptdivc  46473  dvnmul  46478  dvmptfprodlem  46479  dvnprodlem2  46482  stoweidlem59  46594  fourierdlem31  46673  sge00  46911  sge0pnffigt  46931  sge0lefi  46933  sge0resplit  46941  sge0lempt  46945  sge0iunmptlemfi  46948  sge0iunmptlemre  46950  sge0iunmpt  46953  sge0xadd  46970  sge0gtfsumgt  46978  iundjiun  46995  meadjiun  47001  meaiininclem  47021  omeiunltfirp  47054  hoidmvlelem1  47130  hoidmvlelem3  47132  hspdifhsp  47151  hoiqssbllem2  47158  hspmbllem2  47162  opnvonmbllem2  47168  hoimbl2  47200  vonhoire  47207  iinhoiicc  47209  iunhoiioo  47211  vonn0ioo2  47225  vonn0icc2  47227  incsmflem  47276  issmfle  47280  issmfgt  47291  decsmflem  47301  issmfge  47305  smflimlem2  47307  smflim  47312  smfresal  47323  smfpimbor1lem2  47334  smflim2  47341  smflimmpt  47345  smfsuplem1  47346  smfsupxr  47351  smfinflem  47352  smflimsuplem7  47361  smflimsuplem8  47362  smflimsup  47363  smflimsupmpt  47364  smfliminf  47366  smfliminfmpt  47367  nfdfat  47682