Theorem nfel 2916

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1784   ∈ wcel 2105  Ⅎwnfc 2882

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-cleq 2723  df-clel 2809  df-nfc 2884

This theorem is referenced by:  nfel1  2918  nfel2  2920  nfnel  3053  elabgf  3664  elrabf  3679  sbcel12  4408  rabxfrd  5415  ffnfvf  7121  nfixpw  8916  mptelixpg  8935  fsumsplit1  15698  ptcldmpt  23439  prdsdsf  24194  prdsxmet  24196  ssiun2sf  32226  iinabrex  32235  acunirnmpt2  32320  acunirnmpt2f  32321  aciunf1lem  32322  funcnv4mpt  32329  fsumiunle  32470  zarclsiin  33317  esumc  33515  esumrnmpt2  33532  esumgect  33554  esum2dlem  33556  esum2d  33557  esumiun  33558  ldsysgenld  33624  sigapildsys  33626  fiunelros  33638  omssubadd  33765  breprexplema  34108  bnj1491  34534  currysetlem  36293  currysetlem1  36295  ptrest  36954  aomclem8  42269  ss2iundf  42876  elunif  44166  rspcegf  44173  fiiuncl  44217  eliuniincex  44263  disjf1  44344  disjf1o  44352  iunmapsn  44378  fmptf  44404  infnsuprnmpt  44416  fmptff  44436  iuneqfzuzlem  44506  allbutfi  44565  supminfrnmpt  44617  supminfxrrnmpt  44643  monoordxr  44655  monoord2xr  44657  iooiinicc  44717  iooiinioc  44731  fsumiunss  44753  fprodcn  44778  climsuse  44786  climsubmpt  44838  climreclf  44842  fnlimcnv  44845  climeldmeqmpt  44846  climfveqmpt  44849  fnlimfvre  44852  fnlimabslt  44857  climfveqmpt3  44860  climbddf  44865  climeldmeqmpt3  44867  climinf2mpt  44892  climinfmpt  44893  limsupequzmptf  44909  lmbr3  44925  fprodcncf  45078  dvmptmulf  45115  dvnmptdivc  45116  dvnmul  45121  dvmptfprodlem  45122  dvmptfprod  45123  dvnprodlem1  45124  dvnprodlem2  45125  stoweidlem59  45237  fourierdlem31  45316  sge00  45554  sge0f1o  45560  sge0pnffigt  45574  sge0lefi  45576  sge0resplit  45584  sge0lempt  45588  sge0iunmptlemfi  45591  sge0iunmptlemre  45593  sge0iunmpt  45596  sge0xadd  45613  sge0gtfsumgt  45621  iundjiun  45638  meadjiun  45644  meaiininclem  45664  omeiunltfirp  45697  hoidmvlelem1  45773  hoidmvlelem3  45775  hspdifhsp  45794  hoiqssbllem2  45801  hspmbllem2  45805  opnvonmbllem2  45811  hoimbl2  45843  vonhoire  45850  iinhoiicc  45852  iunhoiioo  45854  vonn0ioo2  45868  vonn0icc2  45870  incsmflem  45919  issmfle  45923  issmfgt  45934  decsmflem  45944  issmfge  45948  smflimlem2  45950  smflim  45955  smfresal  45966  smfpimbor1lem2  45977  smflim2  45984  smflimmpt  45988  smfsuplem1  45989  smfsupxr  45994  smfinflem  45995  smfinfmpt  45997  smflimsuplem7  46004  smflimsuplem8  46005  smflimsup  46006  smflimsupmpt  46007  smfliminf  46009  smfliminfmpt  46010  nfdfat  46297