Theorem nfel 2945

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

Syntax hints:  ⊤wtru 1602  Ⅎwnf 1827   ∈ wcel 2106  Ⅎwnfc 2918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-cleq 2769  df-clel 2773  df-nfc 2920

This theorem is referenced by:  nfel1  2947  nfel2  2949  nfnel  3081  elabgf  3553  elrabf  3567  sbcel12  4207  rabxfrd  5129  ffnfvf  6653  mptelixpg  8231  ptcldmpt  21826  prdsdsf  22580  prdsxmet  22582  ssiun2sf  29940  acunirnmpt2  30025  acunirnmpt2f  30026  aciunf1lem  30027  funcnv4mpt  30034  fsumiunle  30139  esumc  30711  esumrnmpt2  30728  esumgect  30750  esum2dlem  30752  esum2d  30753  esumiun  30754  ldsysgenld  30821  sigapildsys  30823  fiunelros  30835  omssubadd  30960  breprexplema  31310  bnj1491  31724  ptrest  34018  aomclem8  38572  ss2iundf  38890  elunif  40090  rspcegf  40097  fiiuncl  40147  cbvmpt21  40191  eliuniincex  40203  iinssiin  40222  iinssf  40235  disjf1  40274  wessf1ornlem  40276  disjrnmpt2  40280  disjf1o  40283  disjinfi  40285  iunmapsn  40312  fmptf  40344  infnsuprnmpt  40358  iuneqfzuzlem  40440  allbutfi  40504  supminfrnmpt  40560  supminfxrrnmpt  40588  monoordxr  40600  monoord2xr  40602  iooiinicc  40659  iooiinioc  40673  fsumsplit1  40694  fsumiunss  40697  fprodcnlem  40721  fprodcn  40722  climsuse  40730  climsubmpt  40782  climreclf  40786  fnlimcnv  40789  climeldmeqmpt  40790  climfveqmpt  40793  fnlimfvre  40796  fnlimabslt  40801  climfveqmpt3  40804  climbddf  40809  climeldmeqmpt3  40811  climinf2mpt  40836  climinfmpt  40837  limsupequzmptf  40853  lmbr3  40869  fprodcncf  41024  dvmptmulf  41062  dvnmptdivc  41063  dvnmul  41068  dvmptfprodlem  41069  dvmptfprod  41070  dvnprodlem1  41071  dvnprodlem2  41072  stoweidlem59  41185  fourierdlem31  41264  sge00  41499  sge0f1o  41505  sge0pnffigt  41519  sge0lefi  41521  sge0resplit  41529  sge0lempt  41533  sge0iunmptlemfi  41536  sge0iunmptlemre  41538  sge0iunmpt  41541  sge0xadd  41558  sge0gtfsumgt  41566  iundjiun  41583  meadjiun  41589  meaiininclem  41609  omeiunltfirp  41642  hoidmvlelem1  41718  hoidmvlelem3  41720  hspdifhsp  41739  hoiqssbllem2  41746  hspmbllem2  41750  opnvonmbllem2  41756  hoimbl2  41788  vonhoire  41795  iinhoiicc  41797  iunhoiioo  41799  vonn0ioo2  41813  vonn0icc2  41815  incsmflem  41859  issmfle  41863  issmfgt  41874  decsmflem  41883  issmfge  41887  smflimlem2  41889  smflim  41894  smfresal  41904  smfpimbor1lem2  41915  smflim2  41921  smflimmpt  41925  smfsuplem1  41926  smfsupmpt  41930  smfsupxr  41931  smfinflem  41932  smfinfmpt  41934  smflimsuplem7  41941  smflimsuplem8  41942  smflimsup  41943  smflimsupmpt  41944  smfliminf  41946  smfliminfmpt  41947  nfdfat  42150