Theorem nfel 2920

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

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1787   ∈ wcel 2108  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-cleq 2730  df-clel 2817  df-nfc 2888

This theorem is referenced by:  nfel1  2922  nfel2  2924  nfnel  3055  elabgf  3598  elrabf  3613  sbcel12  4339  rabxfrd  5335  ffnfvf  6975  nfixpw  8662  mptelixpg  8681  fsumsplit1  15385  ptcldmpt  22673  prdsdsf  23428  prdsxmet  23430  ssiun2sf  30800  iinabrex  30809  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1lem  30901  funcnv4mpt  30908  fsumiunle  31045  zarclsiin  31723  esumc  31919  esumrnmpt2  31936  esumgect  31958  esum2dlem  31960  esum2d  31961  esumiun  31962  ldsysgenld  32028  sigapildsys  32030  fiunelros  32042  omssubadd  32167  breprexplema  32510  bnj1491  32937  currysetlem  35061  currysetlem1  35063  ptrest  35703  aomclem8  40802  ss2iundf  41156  elunif  42448  rspcegf  42455  fiiuncl  42502  eliuniincex  42548  disjf1  42609  disjf1o  42618  iunmapsn  42646  fmptf  42672  infnsuprnmpt  42685  iuneqfzuzlem  42763  allbutfi  42823  supminfrnmpt  42875  supminfxrrnmpt  42901  monoordxr  42913  monoord2xr  42915  iooiinicc  42970  iooiinioc  42984  fsumiunss  43006  fprodcnlem  43030  fprodcn  43031  climsuse  43039  climsubmpt  43091  climreclf  43095  fnlimcnv  43098  climeldmeqmpt  43099  climfveqmpt  43102  fnlimfvre  43105  fnlimabslt  43110  climfveqmpt3  43113  climbddf  43118  climeldmeqmpt3  43120  climinf2mpt  43145  climinfmpt  43146  limsupequzmptf  43162  lmbr3  43178  fprodcncf  43331  dvmptmulf  43368  dvnmptdivc  43369  dvnmul  43374  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem2  43378  stoweidlem59  43490  fourierdlem31  43569  sge00  43804  sge0f1o  43810  sge0pnffigt  43824  sge0lefi  43826  sge0resplit  43834  sge0lempt  43838  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  sge0xadd  43863  sge0gtfsumgt  43871  iundjiun  43888  meadjiun  43894  meaiininclem  43914  omeiunltfirp  43947  hoidmvlelem1  44023  hoidmvlelem3  44025  hspdifhsp  44044  hoiqssbllem2  44051  hspmbllem2  44055  opnvonmbllem2  44061  hoimbl2  44093  vonhoire  44100  iinhoiicc  44102  iunhoiioo  44104  vonn0ioo2  44118  vonn0icc2  44120  incsmflem  44164  issmfle  44168  issmfgt  44179  decsmflem  44188  issmfge  44192  smflimlem2  44194  smflim  44199  smfresal  44209  smfpimbor1lem2  44220  smflim2  44226  smflimmpt  44230  smfsuplem1  44231  smfsupxr  44236  smfinflem  44237  smfinfmpt  44239  smflimsuplem7  44246  smflimsuplem8  44247  smflimsup  44248  smflimsupmpt  44249  smfliminf  44251  smfliminfmpt  44252  nfdfat  44506