Theorem nfel 2909

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784   ∈ wcel 2111  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2723  df-clel 2806  df-nfc 2881

This theorem is referenced by:  nfel1  2911  nfel2  2913  nfnel  3040  elabgf  3625  elrabf  3639  sbcel12  4356  rabxfrd  5350  ffnfvf  7048  nfixpw  8835  mptelixpg  8854  fsumsplit1  15647  ptcldmpt  23524  prdsdsf  24277  prdsxmet  24279  ssiun2sf  32531  iinabrex  32541  acunirnmpt2  32634  acunirnmpt2f  32635  aciunf1lem  32636  funcnv4mpt  32643  fsumiunle  32804  zarclsiin  33876  esumc  34056  esumrnmpt2  34073  esumgect  34095  esum2dlem  34097  esum2d  34098  esumiun  34099  ldsysgenld  34165  sigapildsys  34167  fiunelros  34179  omssubadd  34305  breprexplema  34635  bnj1491  35061  currysetlem  36979  currysetlem1  36981  ptrest  37659  aomclem8  43094  ss2iundf  43692  elunif  45053  rspcegf  45060  fiiuncl  45102  eliuniincex  45146  disjf1  45220  disjf1o  45228  iunmapsn  45254  fmptf  45276  infnsuprnmpt  45287  fmptff  45306  iuneqfzuzlem  45373  allbutfi  45431  supminfrnmpt  45483  supminfxrrnmpt  45509  monoordxr  45520  monoord2xr  45522  iooiinicc  45582  iooiinioc  45596  fsumiunss  45615  fprodcn  45640  climsuse  45648  climsubmpt  45698  climreclf  45702  fnlimcnv  45705  climeldmeqmpt  45706  climfveqmpt  45709  fnlimfvre  45712  fnlimabslt  45717  climfveqmpt3  45720  climbddf  45725  climeldmeqmpt3  45727  climinf2mpt  45752  climinfmpt  45753  limsupequzmptf  45769  lmbr3  45785  fprodcncf  45938  dvmptmulf  45975  dvnmptdivc  45976  dvnmul  45981  dvmptfprodlem  45982  dvnprodlem2  45985  stoweidlem59  46097  fourierdlem31  46176  sge00  46414  sge0pnffigt  46434  sge0lefi  46436  sge0resplit  46444  sge0lempt  46448  sge0iunmptlemfi  46451  sge0iunmptlemre  46453  sge0iunmpt  46456  sge0xadd  46473  sge0gtfsumgt  46481  iundjiun  46498  meadjiun  46504  meaiininclem  46524  omeiunltfirp  46557  hoidmvlelem1  46633  hoidmvlelem3  46635  hspdifhsp  46654  hoiqssbllem2  46661  hspmbllem2  46665  opnvonmbllem2  46671  hoimbl2  46703  vonhoire  46710  iinhoiicc  46712  iunhoiioo  46714  vonn0ioo2  46728  vonn0icc2  46730  incsmflem  46779  issmfle  46783  issmfgt  46794  decsmflem  46804  issmfge  46808  smflimlem2  46810  smflim  46815  smfresal  46826  smfpimbor1lem2  46837  smflim2  46844  smflimmpt  46848  smfsuplem1  46849  smfsupxr  46854  smfinflem  46855  smflimsuplem7  46864  smflimsuplem8  46865  smflimsup  46866  smflimsupmpt  46867  smfliminf  46869  smfliminfmpt  46870  nfdfat  47158