Theorem nfel 2907

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

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2722  df-clel 2804  df-nfc 2879

This theorem is referenced by:  nfel1  2909  nfel2  2911  nfnel  3038  elabgf  3644  elrabf  3658  sbcel12  4377  rabxfrd  5375  ffnfvf  7095  nfixpw  8892  mptelixpg  8911  fsumsplit1  15718  ptcldmpt  23508  prdsdsf  24262  prdsxmet  24264  ssiun2sf  32495  iinabrex  32505  acunirnmpt2  32591  acunirnmpt2f  32592  aciunf1lem  32593  funcnv4mpt  32600  fsumiunle  32761  zarclsiin  33868  esumc  34048  esumrnmpt2  34065  esumgect  34087  esum2dlem  34089  esum2d  34090  esumiun  34091  ldsysgenld  34157  sigapildsys  34159  fiunelros  34171  omssubadd  34298  breprexplema  34628  bnj1491  35054  currysetlem  36940  currysetlem1  36942  ptrest  37620  aomclem8  43057  ss2iundf  43655  elunif  45017  rspcegf  45024  fiiuncl  45066  eliuniincex  45110  disjf1  45184  disjf1o  45192  iunmapsn  45218  fmptf  45240  infnsuprnmpt  45251  fmptff  45270  iuneqfzuzlem  45337  allbutfi  45396  supminfrnmpt  45448  supminfxrrnmpt  45474  monoordxr  45485  monoord2xr  45487  iooiinicc  45547  iooiinioc  45561  fsumiunss  45580  fprodcn  45605  climsuse  45613  climsubmpt  45665  climreclf  45669  fnlimcnv  45672  climeldmeqmpt  45673  climfveqmpt  45676  fnlimfvre  45679  fnlimabslt  45684  climfveqmpt3  45687  climbddf  45692  climeldmeqmpt3  45694  climinf2mpt  45719  climinfmpt  45720  limsupequzmptf  45736  lmbr3  45752  fprodcncf  45905  dvmptmulf  45942  dvnmptdivc  45943  dvnmul  45948  dvmptfprodlem  45949  dvnprodlem2  45952  stoweidlem59  46064  fourierdlem31  46143  sge00  46381  sge0pnffigt  46401  sge0lefi  46403  sge0resplit  46411  sge0lempt  46415  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  sge0xadd  46440  sge0gtfsumgt  46448  iundjiun  46465  meadjiun  46471  meaiininclem  46491  omeiunltfirp  46524  hoidmvlelem1  46600  hoidmvlelem3  46602  hspdifhsp  46621  hoiqssbllem2  46628  hspmbllem2  46632  opnvonmbllem2  46638  hoimbl2  46670  vonhoire  46677  iinhoiicc  46679  iunhoiioo  46681  vonn0ioo2  46695  vonn0icc2  46697  incsmflem  46746  issmfle  46750  issmfgt  46761  decsmflem  46771  issmfge  46775  smflimlem2  46777  smflim  46782  smfresal  46793  smfpimbor1lem2  46804  smflim2  46811  smflimmpt  46815  smfsuplem1  46816  smfsupxr  46821  smfinflem  46822  smflimsuplem7  46831  smflimsuplem8  46832  smflimsup  46833  smflimsupmpt  46834  smfliminf  46836  smfliminfmpt  46837  nfdfat  47132