Theorem nfel 2969

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

Syntax hints:  ⊤wtru 1539  Ⅎwnf 1785   ∈ wcel 2111  Ⅎwnfc 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-clel 2870  df-nfc 2938

This theorem is referenced by:  nfel1  2971  nfel2  2973  nfnel  3098  elabgf  3610  elrabf  3624  sbcel12  4316  rabxfrd  5283  ffnfvf  6860  nfixpw  8463  mptelixpg  8482  ptcldmpt  22219  prdsdsf  22974  prdsxmet  22976  ssiun2sf  30323  iinabrex  30332  acunirnmpt2  30423  acunirnmpt2f  30424  aciunf1lem  30425  funcnv4mpt  30432  fsumiunle  30571  zarclsiin  31224  esumc  31420  esumrnmpt2  31437  esumgect  31459  esum2dlem  31461  esum2d  31462  esumiun  31463  ldsysgenld  31529  sigapildsys  31531  fiunelros  31543  omssubadd  31668  breprexplema  32011  bnj1491  32439  currysetlem  34380  currysetlem1  34382  ptrest  35056  aomclem8  40005  ss2iundf  40360  elunif  41645  rspcegf  41652  fiiuncl  41699  eliuniincex  41745  disjf1  41809  disjf1o  41818  iunmapsn  41846  fmptf  41875  infnsuprnmpt  41888  iuneqfzuzlem  41966  allbutfi  42029  supminfrnmpt  42082  supminfxrrnmpt  42110  monoordxr  42122  monoord2xr  42124  iooiinicc  42179  iooiinioc  42193  fsumsplit1  42214  fsumiunss  42217  fprodcnlem  42241  fprodcn  42242  climsuse  42250  climsubmpt  42302  climreclf  42306  fnlimcnv  42309  climeldmeqmpt  42310  climfveqmpt  42313  fnlimfvre  42316  fnlimabslt  42321  climfveqmpt3  42324  climbddf  42329  climeldmeqmpt3  42331  climinf2mpt  42356  climinfmpt  42357  limsupequzmptf  42373  lmbr3  42389  fprodcncf  42542  dvmptmulf  42579  dvnmptdivc  42580  dvnmul  42585  dvmptfprodlem  42586  dvmptfprod  42587  dvnprodlem1  42588  dvnprodlem2  42589  stoweidlem59  42701  fourierdlem31  42780  sge00  43015  sge0f1o  43021  sge0pnffigt  43035  sge0lefi  43037  sge0resplit  43045  sge0lempt  43049  sge0iunmptlemfi  43052  sge0iunmptlemre  43054  sge0iunmpt  43057  sge0xadd  43074  sge0gtfsumgt  43082  iundjiun  43099  meadjiun  43105  meaiininclem  43125  omeiunltfirp  43158  hoidmvlelem1  43234  hoidmvlelem3  43236  hspdifhsp  43255  hoiqssbllem2  43262  hspmbllem2  43266  opnvonmbllem2  43272  hoimbl2  43304  vonhoire  43311  iinhoiicc  43313  iunhoiioo  43315  vonn0ioo2  43329  vonn0icc2  43331  incsmflem  43375  issmfle  43379  issmfgt  43390  decsmflem  43399  issmfge  43403  smflimlem2  43405  smflim  43410  smfresal  43420  smfpimbor1lem2  43431  smflim2  43437  smflimmpt  43441  smfsuplem1  43442  smfsupmpt  43446  smfsupxr  43447  smfinflem  43448  smfinfmpt  43450  smflimsuplem7  43457  smflimsuplem8  43458  smflimsup  43459  smflimsupmpt  43460  smfliminf  43462  smfliminfmpt  43463  nfdfat  43683