Theorem nfel 2936

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1815   ∈ wcel 2144  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-cleq 2752  df-clel 2835  df-nfc 2909

This theorem is used by:  nfel1  2938  nfel2  2940  nfnel  3069  elabgf  3627  elrabf  3641  sbcel12  4368  rabxfrd  5378  ffnfvf  7121  nfixpw  8948  mptelixpg  8967  fsumsplit1  15917  ptcldmpt  23939  prdsdsf  24692  prdsxmet  24694  ssiun2sf  33202  iinabrex  33211  aciunf1lem  33304  funcnv4mpt  33310  fsumiunle  33467  zarclsiin  34550  esumc  34730  esumrnmpt2  34747  esumgect  34769  esum2dlem  34771  esum2d  34772  esumiun  34773  ldsysgenld  34840  sigapildsys  34842  fiunelros  34854  breprexplema  35306  bnj1491  35734  currysetlem  37951  currysetlem1  37953  ptrest  38631  aomclem8  44157  ss2iundf  44753  elunif  46127  rspcegf  46134  fiiuncl  46176  eliuniincex  46218  disjf1  46292  disjf1o  46300  iunmapsn  46324  fmptf  46345  infnsuprnmpt  46356  fmptff  46375  iuneqfzuzlem  46440  allbutfi  46498  supminfrnmpt  46549  supminfxrrnmpt  46575  monoordxr  46586  monoord2xr  46588  iooiinicc  46648  iooiinioc  46662  fsumiunss  46681  fprodcn  46706  climsuse  46714  climsubmpt  46764  climreclf  46768  fnlimcnv  46771  climeldmeqmpt  46772  climfveqmpt  46775  fnlimfvre  46778  fnlimabslt  46783  climfveqmpt3  46786  climbddf  46791  climeldmeqmpt3  46793  climinf2mpt  46818  climinfmpt  46819  limsupequzmptf  46835  lmbr3  46851  fprodcncf  47004  dvmptmulf  47041  dvnmptdivc  47042  dvnmul  47047  dvmptfprodlem  47048  dvnprodlem2  47051  stoweidlem59  47163  fourierdlem31  47242  sge00  47480  sge0pnffigt  47500  sge0lefi  47502  sge0resplit  47510  sge0lempt  47514  sge0iunmptlemfi  47517  sge0iunmptlemre  47519  sge0iunmpt  47522  sge0xadd  47539  sge0gtfsumgt  47547  iundjiun  47564  meadjiun  47570  meaiininclem  47590  omeiunltfirp  47623  hoidmvlelem1  47699  hoidmvlelem3  47701  hspdifhsp  47720  hoiqssbllem2  47727  hspmbllem2  47731  opnvonmbllem2  47737  hoimbl2  47769  vonhoire  47776  iinhoiicc  47778  iunhoiioo  47780  vonn0ioo2  47794  vonn0icc2  47796  incsmflem  47845  issmfle  47849  issmfgt  47860  decsmflem  47870  issmfge  47874  smflimlem2  47876  smflim  47881  smfresal  47892  smfpimbor1lem2  47903  smflim2  47910  smflimmpt  47914  smfsuplem1  47915  smfsupxr  47920  smfinflem  47921  smflimsuplem7  47930  smflimsuplem8  47931  smflimsup  47932  smflimsupmpt  47933  smfliminf  47935  smfliminfmpt  47936  nfdfat  48291