Theorem nfel 2923

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

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-cleq 2732  df-clel 2819  df-nfc 2895

This theorem is referenced by:  nfel1  2925  nfel2  2927  nfnel  3060  elabgf  3688  elrabf  3704  sbcel12  4434  rabxfrd  5435  ffnfvf  7154  nfixpw  8974  mptelixpg  8993  fsumsplit1  15793  ptcldmpt  23643  prdsdsf  24398  prdsxmet  24400  ssiun2sf  32582  iinabrex  32591  acunirnmpt2  32678  acunirnmpt2f  32679  aciunf1lem  32680  funcnv4mpt  32687  fsumiunle  32833  zarclsiin  33817  esumc  34015  esumrnmpt2  34032  esumgect  34054  esum2dlem  34056  esum2d  34057  esumiun  34058  ldsysgenld  34124  sigapildsys  34126  fiunelros  34138  omssubadd  34265  breprexplema  34607  bnj1491  35033  currysetlem  36911  currysetlem1  36913  ptrest  37579  aomclem8  43018  ss2iundf  43621  elunif  44916  rspcegf  44923  fiiuncl  44967  eliuniincex  45011  disjf1  45090  disjf1o  45098  iunmapsn  45124  fmptf  45147  infnsuprnmpt  45159  fmptff  45179  iuneqfzuzlem  45249  allbutfi  45308  supminfrnmpt  45360  supminfxrrnmpt  45386  monoordxr  45398  monoord2xr  45400  iooiinicc  45460  iooiinioc  45474  fsumiunss  45496  fprodcn  45521  climsuse  45529  climsubmpt  45581  climreclf  45585  fnlimcnv  45588  climeldmeqmpt  45589  climfveqmpt  45592  fnlimfvre  45595  fnlimabslt  45600  climfveqmpt3  45603  climbddf  45608  climeldmeqmpt3  45610  climinf2mpt  45635  climinfmpt  45636  limsupequzmptf  45652  lmbr3  45668  fprodcncf  45821  dvmptmulf  45858  dvnmptdivc  45859  dvnmul  45864  dvmptfprodlem  45865  dvmptfprod  45866  dvnprodlem1  45867  dvnprodlem2  45868  stoweidlem59  45980  fourierdlem31  46059  sge00  46297  sge0f1o  46303  sge0pnffigt  46317  sge0lefi  46319  sge0resplit  46327  sge0lempt  46331  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  sge0xadd  46356  sge0gtfsumgt  46364  iundjiun  46381  meadjiun  46387  meaiininclem  46407  omeiunltfirp  46440  hoidmvlelem1  46516  hoidmvlelem3  46518  hspdifhsp  46537  hoiqssbllem2  46544  hspmbllem2  46548  opnvonmbllem2  46554  hoimbl2  46586  vonhoire  46593  iinhoiicc  46595  iunhoiioo  46597  vonn0ioo2  46611  vonn0icc2  46613  incsmflem  46662  issmfle  46666  issmfgt  46677  decsmflem  46687  issmfge  46691  smflimlem2  46693  smflim  46698  smfresal  46709  smfpimbor1lem2  46720  smflim2  46727  smflimmpt  46731  smfsuplem1  46732  smfsupxr  46737  smfinflem  46738  smfinfmpt  46740  smflimsuplem7  46747  smflimsuplem8  46748  smflimsup  46749  smflimsupmpt  46750  smfliminf  46752  smfliminfmpt  46753  nfdfat  47042