Theorem nfel 2922

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

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-cleq 2731  df-clel 2817  df-nfc 2890

This theorem is referenced by:  nfel1  2924  nfel2  2926  nfnel  3057  elabgf  3606  elrabf  3621  sbcel12  4343  rabxfrd  5341  ffnfvf  7002  nfixpw  8713  mptelixpg  8732  fsumsplit1  15466  ptcldmpt  22774  prdsdsf  23529  prdsxmet  23531  ssiun2sf  30908  iinabrex  30917  acunirnmpt2  31006  acunirnmpt2f  31007  aciunf1lem  31008  funcnv4mpt  31015  fsumiunle  31152  zarclsiin  31830  esumc  32028  esumrnmpt2  32045  esumgect  32067  esum2dlem  32069  esum2d  32070  esumiun  32071  ldsysgenld  32137  sigapildsys  32139  fiunelros  32151  omssubadd  32276  breprexplema  32619  bnj1491  33046  currysetlem  35143  currysetlem1  35145  ptrest  35785  aomclem8  40893  ss2iundf  41274  elunif  42566  rspcegf  42573  fiiuncl  42620  eliuniincex  42666  disjf1  42727  disjf1o  42736  iunmapsn  42764  fmptf  42790  infnsuprnmpt  42803  iuneqfzuzlem  42880  allbutfi  42940  supminfrnmpt  42992  supminfxrrnmpt  43018  monoordxr  43030  monoord2xr  43032  iooiinicc  43087  iooiinioc  43101  fsumiunss  43123  fprodcnlem  43147  fprodcn  43148  climsuse  43156  climsubmpt  43208  climreclf  43212  fnlimcnv  43215  climeldmeqmpt  43216  climfveqmpt  43219  fnlimfvre  43222  fnlimabslt  43227  climfveqmpt3  43230  climbddf  43235  climeldmeqmpt3  43237  climinf2mpt  43262  climinfmpt  43263  limsupequzmptf  43279  lmbr3  43295  fprodcncf  43448  dvmptmulf  43485  dvnmptdivc  43486  dvnmul  43491  dvmptfprodlem  43492  dvmptfprod  43493  dvnprodlem1  43494  dvnprodlem2  43495  stoweidlem59  43607  fourierdlem31  43686  sge00  43921  sge0f1o  43927  sge0pnffigt  43941  sge0lefi  43943  sge0resplit  43951  sge0lempt  43955  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0iunmpt  43963  sge0xadd  43980  sge0gtfsumgt  43988  iundjiun  44005  meadjiun  44011  meaiininclem  44031  omeiunltfirp  44064  hoidmvlelem1  44140  hoidmvlelem3  44142  hspdifhsp  44161  hoiqssbllem2  44168  hspmbllem2  44172  opnvonmbllem2  44178  hoimbl2  44210  vonhoire  44217  iinhoiicc  44219  iunhoiioo  44221  vonn0ioo2  44235  vonn0icc2  44237  incsmflem  44286  issmfle  44290  issmfgt  44301  decsmflem  44311  issmfge  44315  smflimlem2  44317  smflim  44322  smfresal  44333  smfpimbor1lem2  44344  smflim2  44350  smflimmpt  44354  smfsuplem1  44355  smfsupxr  44360  smfinflem  44361  smfinfmpt  44363  smflimsuplem7  44370  smflimsuplem8  44371  smflimsup  44372  smflimsupmpt  44373  smfliminf  44375  smfliminfmpt  44376  nfdfat  44630