Theorem nfel 2913

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 2910	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 ∈ 𝐵)
6	5	mptru 1549	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1790   ∈ wcel 2113  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-cleq 2730  df-clel 2811  df-nfc 2881

This theorem is referenced by:  nfel1  2915  nfel2  2917  nfnel  3045  elabgf  3566  elrabf  3581  sbcel12  4295  rabxfrd  5281  ffnfvf  6887  nfixpw  8519  mptelixpg  8538  ptcldmpt  22358  prdsdsf  23113  prdsxmet  23115  ssiun2sf  30465  iinabrex  30474  acunirnmpt2  30564  acunirnmpt2f  30565  aciunf1lem  30566  funcnv4mpt  30573  fsumiunle  30710  zarclsiin  31385  esumc  31581  esumrnmpt2  31598  esumgect  31620  esum2dlem  31622  esum2d  31623  esumiun  31624  ldsysgenld  31690  sigapildsys  31692  fiunelros  31704  omssubadd  31829  breprexplema  32172  bnj1491  32600  currysetlem  34746  currysetlem1  34748  ptrest  35388  aomclem8  40442  ss2iundf  40797  elunif  42081  rspcegf  42088  fiiuncl  42135  eliuniincex  42181  disjf1  42242  disjf1o  42251  iunmapsn  42279  fmptf  42304  infnsuprnmpt  42317  iuneqfzuzlem  42395  allbutfi  42455  supminfrnmpt  42507  supminfxrrnmpt  42535  monoordxr  42547  monoord2xr  42549  iooiinicc  42604  iooiinioc  42618  fsumsplit1  42639  fsumiunss  42642  fprodcnlem  42666  fprodcn  42667  climsuse  42675  climsubmpt  42727  climreclf  42731  fnlimcnv  42734  climeldmeqmpt  42735  climfveqmpt  42738  fnlimfvre  42741  fnlimabslt  42746  climfveqmpt3  42749  climbddf  42754  climeldmeqmpt3  42756  climinf2mpt  42781  climinfmpt  42782  limsupequzmptf  42798  lmbr3  42814  fprodcncf  42967  dvmptmulf  43004  dvnmptdivc  43005  dvnmul  43010  dvmptfprodlem  43011  dvmptfprod  43012  dvnprodlem1  43013  dvnprodlem2  43014  stoweidlem59  43126  fourierdlem31  43205  sge00  43440  sge0f1o  43446  sge0pnffigt  43460  sge0lefi  43462  sge0resplit  43470  sge0lempt  43474  sge0iunmptlemfi  43477  sge0iunmptlemre  43479  sge0iunmpt  43482  sge0xadd  43499  sge0gtfsumgt  43507  iundjiun  43524  meadjiun  43530  meaiininclem  43550  omeiunltfirp  43583  hoidmvlelem1  43659  hoidmvlelem3  43661  hspdifhsp  43680  hoiqssbllem2  43687  hspmbllem2  43691  opnvonmbllem2  43697  hoimbl2  43729  vonhoire  43736  iinhoiicc  43738  iunhoiioo  43740  vonn0ioo2  43754  vonn0icc2  43756  incsmflem  43800  issmfle  43804  issmfgt  43815  decsmflem  43824  issmfge  43828  smflimlem2  43830  smflim  43835  smfresal  43845  smfpimbor1lem2  43856  smflim2  43862  smflimmpt  43866  smfsuplem1  43867  smfsupmpt  43871  smfsupxr  43872  smfinflem  43873  smfinfmpt  43875  smflimsuplem7  43882  smflimsuplem8  43883  smflimsup  43884  smflimsupmpt  43885  smfliminf  43887  smfliminfmpt  43888  nfdfat  44136