Theorem nfel1 2323

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

Syntax hints:  Ⅎwnf 1453   ∈ wcel 2141  Ⅎwnfc 2299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-cleq 2163  df-clel 2166  df-nfc 2301

This theorem is referenced by:  vtocl2gf  2792  vtocl3gf  2793  vtoclgaf  2795  vtocl2gaf  2797  vtocl3gaf  2799  nfop  3781  pofun  4297  nfse  4326  rabxfrd  4454  mptfvex  5581  fvmptf  5588  fmptcof  5663  fliftfuns  5777  riota2f  5830  ovmpos  5976  ov2gf  5977  fmpox  6179  mpofvex  6182  qliftfuns  6597  xpf1o  6822  iunfidisj  6923  cc3  7230  sumfct  11337  sumrbdclem  11340  summodclem3  11343  summodclem2a  11344  zsumdc  11347  fsumgcl  11349  fsum3  11350  isumss  11354  isumss2  11356  fsum3cvg2  11357  fsumsplitf  11371  fsum2dlemstep  11397  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  fsummulc2  11411  fsum00  11425  fsumabs  11428  fsumrelem  11434  fsumiun  11440  isumshft  11453  mertenslem2  11499  prodrbdclem  11534  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  prodfct  11550  prodssdc  11552  fprodmul  11554  fprodm1s  11564  fprodp1s  11565  fprodcl2lem  11568  fprodabs  11579  fprod2dlemstep  11585  fprodcom2fi  11589  fprodrec  11592  fproddivapf  11594  fprodsplitf  11595  fprodsplit1f  11597  fprodle  11603  infssuzcldc  11906  pcmpt  12295  pcmptdvds  12297  iuncld  12909  fsumcncntop  13350