Theorem nfel 2910

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

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2880

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

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 2725  df-clel 2808  df-nfc 2882

This theorem is referenced by:  nfel1  2912  nfel2  2914  nfnel  3041  elabgf  3626  elrabf  3640  sbcel12  4360  rabxfrd  5359  ffnfvf  7062  nfixpw  8850  mptelixpg  8869  fsumsplit1  15659  ptcldmpt  23549  prdsdsf  24302  prdsxmet  24304  ssiun2sf  32560  iinabrex  32570  acunirnmpt2  32664  acunirnmpt2f  32665  aciunf1lem  32666  funcnv4mpt  32673  fsumiunle  32838  zarclsiin  33956  esumc  34136  esumrnmpt2  34153  esumgect  34175  esum2dlem  34177  esum2d  34178  esumiun  34179  ldsysgenld  34245  sigapildsys  34247  fiunelros  34259  omssubadd  34385  breprexplema  34715  bnj1491  35141  currysetlem  37062  currysetlem1  37064  ptrest  37732  aomclem8  43218  ss2iundf  43816  elunif  45177  rspcegf  45184  fiiuncl  45226  eliuniincex  45269  disjf1  45343  disjf1o  45351  iunmapsn  45377  fmptf  45399  infnsuprnmpt  45410  fmptff  45429  iuneqfzuzlem  45495  allbutfi  45553  supminfrnmpt  45605  supminfxrrnmpt  45631  monoordxr  45642  monoord2xr  45644  iooiinicc  45704  iooiinioc  45718  fsumiunss  45737  fprodcn  45762  climsuse  45770  climsubmpt  45820  climreclf  45824  fnlimcnv  45827  climeldmeqmpt  45828  climfveqmpt  45831  fnlimfvre  45834  fnlimabslt  45839  climfveqmpt3  45842  climbddf  45847  climeldmeqmpt3  45849  climinf2mpt  45874  climinfmpt  45875  limsupequzmptf  45891  lmbr3  45907  fprodcncf  46060  dvmptmulf  46097  dvnmptdivc  46098  dvnmul  46103  dvmptfprodlem  46104  dvnprodlem2  46107  stoweidlem59  46219  fourierdlem31  46298  sge00  46536  sge0pnffigt  46556  sge0lefi  46558  sge0resplit  46566  sge0lempt  46570  sge0iunmptlemfi  46573  sge0iunmptlemre  46575  sge0iunmpt  46578  sge0xadd  46595  sge0gtfsumgt  46603  iundjiun  46620  meadjiun  46626  meaiininclem  46646  omeiunltfirp  46679  hoidmvlelem1  46755  hoidmvlelem3  46757  hspdifhsp  46776  hoiqssbllem2  46783  hspmbllem2  46787  opnvonmbllem2  46793  hoimbl2  46825  vonhoire  46832  iinhoiicc  46834  iunhoiioo  46836  vonn0ioo2  46850  vonn0icc2  46852  incsmflem  46901  issmfle  46905  issmfgt  46916  decsmflem  46926  issmfge  46930  smflimlem2  46932  smflim  46937  smfresal  46948  smfpimbor1lem2  46959  smflim2  46966  smflimmpt  46970  smfsuplem1  46971  smfsupxr  46976  smfinflem  46977  smflimsuplem7  46986  smflimsuplem8  46987  smflimsup  46988  smflimsupmpt  46989  smfliminf  46991  smfliminfmpt  46992  nfdfat  47289