Theorem nfel1 2358

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 2347	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2356	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1482   ∈ wcel 2175  Ⅎwnfc 2334

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-cleq 2197  df-clel 2200  df-nfc 2336

This theorem is referenced by:  vtocl2gf  2834  vtocl3gf  2835  vtoclgaf  2837  vtocl2gaf  2839  vtocl3gaf  2841  nfop  3834  pofun  4358  nfse  4387  rabxfrd  4515  mptfvex  5664  fvmptf  5671  fmptcof  5746  fliftfuns  5866  riota2f  5920  ovmpos  6068  ov2gf  6069  elovmporab  6145  elovmporab1w  6146  fmpox  6285  mpofvex  6290  qliftfuns  6705  xpf1o  6940  iunfidisj  7047  cc3  7379  infssuzcldc  10376  sumfct  11656  sumrbdclem  11659  summodclem3  11662  summodclem2a  11663  zsumdc  11666  fsumgcl  11668  fsum3  11669  isumss  11673  isumss2  11675  fsum3cvg2  11676  fsumsplitf  11690  fsum2dlemstep  11716  fisumcom2  11720  fsumshftm  11727  fisum0diag2  11729  fsummulc2  11730  fsum00  11744  fsumabs  11747  fsumrelem  11753  fsumiun  11759  isumshft  11772  mertenslem2  11818  prodrbdclem  11853  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  prodfct  11869  prodssdc  11871  fprodmul  11873  fprodm1s  11883  fprodp1s  11884  fprodcl2lem  11887  fprodabs  11898  fprod2dlemstep  11904  fprodcom2fi  11908  fprodrec  11911  fproddivapf  11913  fprodsplitf  11914  fprodsplit1f  11916  fprodle  11922  pcmpt  12637  pcmptdvds  12639  gsumfzfsumlemm  14320  iuncld  14558  fsumcncntop  15010  dvmptfsum  15168