Theorem nfel1 2359

Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq1.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfel1	⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Distinct variable group:   𝑥,𝐵

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfel1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2348	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2357	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1483   ∈ wcel 2176  Ⅎwnfc 2335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337

This theorem is referenced by:  vtocl2gf  2835  vtocl3gf  2836  vtoclgaf  2838  vtocl2gaf  2840  vtocl3gaf  2842  nfop  3835  pofun  4359  nfse  4388  rabxfrd  4516  mptfvex  5665  fvmptf  5672  fmptcof  5747  fliftfuns  5867  riota2f  5921  ovmpos  6069  ov2gf  6070  elovmporab  6146  elovmporab1w  6147  fmpox  6286  mpofvex  6291  qliftfuns  6706  xpf1o  6941  iunfidisj  7048  cc3  7380  infssuzcldc  10378  sumfct  11685  sumrbdclem  11688  summodclem3  11691  summodclem2a  11692  zsumdc  11695  fsumgcl  11697  fsum3  11698  isumss  11702  isumss2  11704  fsum3cvg2  11705  fsumsplitf  11719  fsum2dlemstep  11745  fisumcom2  11749  fsumshftm  11756  fisum0diag2  11758  fsummulc2  11759  fsum00  11773  fsumabs  11776  fsumrelem  11782  fsumiun  11788  isumshft  11801  mertenslem2  11847  prodrbdclem  11882  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  prodfct  11898  prodssdc  11900  fprodmul  11902  fprodm1s  11912  fprodp1s  11913  fprodcl2lem  11916  fprodabs  11927  fprod2dlemstep  11933  fprodcom2fi  11937  fprodrec  11940  fproddivapf  11942  fprodsplitf  11943  fprodsplit1f  11945  fprodle  11951  pcmpt  12666  pcmptdvds  12668  gsumfzfsumlemm  14349  iuncld  14587  fsumcncntop  15039  dvmptfsum  15197