Theorem nfel 2914

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

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-clel 2812  df-nfc 2886

This theorem is referenced by:  nfel1  2916  nfel2  2918  nfnel  3045  elabgf  3631  elrabf  3645  sbcel12  4365  rabxfrd  5364  ffnfvf  7074  nfixpw  8866  mptelixpg  8885  fsumsplit1  15680  ptcldmpt  23570  prdsdsf  24323  prdsxmet  24325  ssiun2sf  32645  iinabrex  32655  acunirnmpt2  32749  acunirnmpt2f  32750  aciunf1lem  32751  funcnv4mpt  32757  fsumiunle  32920  zarclsiin  34048  esumc  34228  esumrnmpt2  34245  esumgect  34267  esum2dlem  34269  esum2d  34270  esumiun  34271  ldsysgenld  34337  sigapildsys  34339  fiunelros  34351  omssubadd  34477  breprexplema  34807  bnj1491  35232  currysetlem  37190  currysetlem1  37192  ptrest  37867  aomclem8  43415  ss2iundf  44012  elunif  45373  rspcegf  45380  fiiuncl  45422  eliuniincex  45465  disjf1  45539  disjf1o  45547  iunmapsn  45572  fmptf  45594  infnsuprnmpt  45605  fmptff  45624  iuneqfzuzlem  45690  allbutfi  45748  supminfrnmpt  45800  supminfxrrnmpt  45826  monoordxr  45837  monoord2xr  45839  iooiinicc  45899  iooiinioc  45913  fsumiunss  45932  fprodcn  45957  climsuse  45965  climsubmpt  46015  climreclf  46019  fnlimcnv  46022  climeldmeqmpt  46023  climfveqmpt  46026  fnlimfvre  46029  fnlimabslt  46034  climfveqmpt3  46037  climbddf  46042  climeldmeqmpt3  46044  climinf2mpt  46069  climinfmpt  46070  limsupequzmptf  46086  lmbr3  46102  fprodcncf  46255  dvmptmulf  46292  dvnmptdivc  46293  dvnmul  46298  dvmptfprodlem  46299  dvnprodlem2  46302  stoweidlem59  46414  fourierdlem31  46493  sge00  46731  sge0pnffigt  46751  sge0lefi  46753  sge0resplit  46761  sge0lempt  46765  sge0iunmptlemfi  46768  sge0iunmptlemre  46770  sge0iunmpt  46773  sge0xadd  46790  sge0gtfsumgt  46798  iundjiun  46815  meadjiun  46821  meaiininclem  46841  omeiunltfirp  46874  hoidmvlelem1  46950  hoidmvlelem3  46952  hspdifhsp  46971  hoiqssbllem2  46978  hspmbllem2  46982  opnvonmbllem2  46988  hoimbl2  47020  vonhoire  47027  iinhoiicc  47029  iunhoiioo  47031  vonn0ioo2  47045  vonn0icc2  47047  incsmflem  47096  issmfle  47100  issmfgt  47111  decsmflem  47121  issmfge  47125  smflimlem2  47127  smflim  47132  smfresal  47143  smfpimbor1lem2  47154  smflim2  47161  smflimmpt  47165  smfsuplem1  47166  smfsupxr  47171  smfinflem  47172  smflimsuplem7  47181  smflimsuplem8  47182  smflimsup  47183  smflimsupmpt  47184  smfliminf  47186  smfliminfmpt  47187  nfdfat  47484