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  7120  nfixpw  8944  mptelixpg  8963  fsumsplit1  15911  ptcldmpt  23933  prdsdsf  24686  prdsxmet  24688  ssiun2sf  33196  iinabrex  33205  acunirnmpt2  33296  acunirnmpt2f  33297  aciunf1lem  33298  funcnv4mpt  33304  fsumiunle  33462  zarclsiin  34545  esumc  34725  esumrnmpt2  34742  esumgect  34764  esum2dlem  34766  esum2d  34767  esumiun  34768  ldsysgenld  34835  sigapildsys  34837  fiunelros  34849  omssubadd  34974  breprexplema  35301  bnj1491  35729  currysetlem  37900  currysetlem1  37902  ptrest  38580  aomclem8  44105  ss2iundf  44701  elunif  46075  rspcegf  46082  fiiuncl  46124  eliuniincex  46166  disjf1  46240  disjf1o  46248  iunmapsn  46272  fmptf  46293  infnsuprnmpt  46304  fmptff  46323  iuneqfzuzlem  46388  allbutfi  46446  supminfrnmpt  46497  supminfxrrnmpt  46523  monoordxr  46534  monoord2xr  46536  iooiinicc  46596  iooiinioc  46610  fsumiunss  46629  fprodcn  46654  climsuse  46662  climsubmpt  46712  climreclf  46716  fnlimcnv  46719  climeldmeqmpt  46720  climfveqmpt  46723  fnlimfvre  46726  fnlimabslt  46731  climfveqmpt3  46734  climbddf  46739  climeldmeqmpt3  46741  climinf2mpt  46766  climinfmpt  46767  limsupequzmptf  46783  lmbr3  46799  fprodcncf  46952  dvmptmulf  46989  dvnmptdivc  46990  dvnmul  46995  dvmptfprodlem  46996  dvnprodlem2  46999  stoweidlem59  47111  fourierdlem31  47190  sge00  47428  sge0pnffigt  47448  sge0lefi  47450  sge0resplit  47458  sge0lempt  47462  sge0iunmptlemfi  47465  sge0iunmptlemre  47467  sge0iunmpt  47470  sge0xadd  47487  sge0gtfsumgt  47495  iundjiun  47512  meadjiun  47518  meaiininclem  47538  omeiunltfirp  47571  hoidmvlelem1  47647  hoidmvlelem3  47649  hspdifhsp  47668  hoiqssbllem2  47675  hspmbllem2  47679  opnvonmbllem2  47685  hoimbl2  47717  vonhoire  47724  iinhoiicc  47726  iunhoiioo  47728  vonn0ioo2  47742  vonn0icc2  47744  incsmflem  47793  issmfle  47797  issmfgt  47808  decsmflem  47818  issmfge  47822  smflimlem2  47824  smflim  47829  smfresal  47840  smfpimbor1lem2  47851  smflim2  47858  smflimmpt  47862  smfsuplem1  47863  smfsupxr  47868  smfinflem  47869  smflimsuplem7  47878  smflimsuplem8  47879  smflimsup  47880  smflimsupmpt  47881  smfliminf  47883  smfliminfmpt  47884  nfdfat  48239