Theorem nfel 2917

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

Syntax hints:  ⊤wtru 1537  Ⅎwnf 1779   ∈ wcel 2105  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-cleq 2726  df-clel 2813  df-nfc 2889

This theorem is referenced by:  nfel1  2919  nfel2  2921  nfnel  3051  elabgf  3674  elrabf  3690  sbcel12  4416  rabxfrd  5422  ffnfvf  7139  nfixpw  8954  mptelixpg  8973  fsumsplit1  15777  ptcldmpt  23637  prdsdsf  24392  prdsxmet  24394  ssiun2sf  32579  iinabrex  32588  acunirnmpt2  32676  acunirnmpt2f  32677  aciunf1lem  32678  funcnv4mpt  32685  fsumiunle  32835  zarclsiin  33831  esumc  34031  esumrnmpt2  34048  esumgect  34070  esum2dlem  34072  esum2d  34073  esumiun  34074  ldsysgenld  34140  sigapildsys  34142  fiunelros  34154  omssubadd  34281  breprexplema  34623  bnj1491  35049  currysetlem  36927  currysetlem1  36929  ptrest  37605  aomclem8  43049  ss2iundf  43648  elunif  44953  rspcegf  44960  fiiuncl  45004  eliuniincex  45048  disjf1  45125  disjf1o  45133  iunmapsn  45159  fmptf  45182  infnsuprnmpt  45194  fmptff  45214  iuneqfzuzlem  45283  allbutfi  45342  supminfrnmpt  45394  supminfxrrnmpt  45420  monoordxr  45432  monoord2xr  45434  iooiinicc  45494  iooiinioc  45508  fsumiunss  45530  fprodcn  45555  climsuse  45563  climsubmpt  45615  climreclf  45619  fnlimcnv  45622  climeldmeqmpt  45623  climfveqmpt  45626  fnlimfvre  45629  fnlimabslt  45634  climfveqmpt3  45637  climbddf  45642  climeldmeqmpt3  45644  climinf2mpt  45669  climinfmpt  45670  limsupequzmptf  45686  lmbr3  45702  fprodcncf  45855  dvmptmulf  45892  dvnmptdivc  45893  dvnmul  45898  dvmptfprodlem  45899  dvnprodlem2  45902  stoweidlem59  46014  fourierdlem31  46093  sge00  46331  sge0pnffigt  46351  sge0lefi  46353  sge0resplit  46361  sge0lempt  46365  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  sge0xadd  46390  sge0gtfsumgt  46398  iundjiun  46415  meadjiun  46421  meaiininclem  46441  omeiunltfirp  46474  hoidmvlelem1  46550  hoidmvlelem3  46552  hspdifhsp  46571  hoiqssbllem2  46578  hspmbllem2  46582  opnvonmbllem2  46588  hoimbl2  46620  vonhoire  46627  iinhoiicc  46629  iunhoiioo  46631  vonn0ioo2  46645  vonn0icc2  46647  incsmflem  46696  issmfle  46700  issmfgt  46711  decsmflem  46721  issmfge  46725  smflimlem2  46727  smflim  46732  smfresal  46743  smfpimbor1lem2  46754  smflim2  46761  smflimmpt  46765  smfsuplem1  46766  smfsupxr  46771  smfinflem  46772  smflimsuplem7  46781  smflimsuplem8  46782  smflimsup  46783  smflimsupmpt  46784  smfliminf  46786  smfliminfmpt  46787  nfdfat  47076