Theorem nfel1 2330

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

Syntax hints:  Ⅎwnf 1460   ∈ wcel 2148  Ⅎwnfc 2306

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308

This theorem is referenced by:  vtocl2gf  2799  vtocl3gf  2800  vtoclgaf  2802  vtocl2gaf  2804  vtocl3gaf  2806  nfop  3793  pofun  4310  nfse  4339  rabxfrd  4467  mptfvex  5598  fvmptf  5605  fmptcof  5680  fliftfuns  5794  riota2f  5847  ovmpos  5993  ov2gf  5994  fmpox  6196  mpofvex  6199  qliftfuns  6614  xpf1o  6839  iunfidisj  6940  cc3  7262  sumfct  11373  sumrbdclem  11376  summodclem3  11379  summodclem2a  11380  zsumdc  11383  fsumgcl  11385  fsum3  11386  isumss  11390  isumss2  11392  fsum3cvg2  11393  fsumsplitf  11407  fsum2dlemstep  11433  fisumcom2  11437  fsumshftm  11444  fisum0diag2  11446  fsummulc2  11447  fsum00  11461  fsumabs  11464  fsumrelem  11470  fsumiun  11476  isumshft  11489  mertenslem2  11535  prodrbdclem  11570  prodmodclem3  11574  prodmodclem2a  11575  zproddc  11578  fprodseq  11582  prodfct  11586  prodssdc  11588  fprodmul  11590  fprodm1s  11600  fprodp1s  11601  fprodcl2lem  11604  fprodabs  11615  fprod2dlemstep  11621  fprodcom2fi  11625  fprodrec  11628  fproddivapf  11630  fprodsplitf  11631  fprodsplit1f  11633  fprodle  11639  infssuzcldc  11942  pcmpt  12331  pcmptdvds  12333  iuncld  13397  fsumcncntop  13838