Theorem nfel1 2383

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

Syntax hints:  Ⅎwnf 1506   ∈ wcel 2200  Ⅎwnfc 2359

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361

This theorem is referenced by:  vtocl2gf  2863  vtocl3gf  2864  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  nfop  3873  pofun  4403  nfse  4432  rabxfrd  4560  mptfvex  5722  fvmptf  5729  fmptcof  5804  fliftfuns  5928  riota2f  5983  ovmpos  6134  ov2gf  6135  elovmporab  6211  elovmporab1w  6212  fmpox  6352  mpofvex  6357  qliftfuns  6774  xpf1o  7013  iunfidisj  7124  cc3  7465  infssuzcldc  10467  sumfct  11900  sumrbdclem  11903  summodclem3  11906  summodclem2a  11907  zsumdc  11910  fsumgcl  11912  fsum3  11913  isumss  11917  isumss2  11919  fsum3cvg2  11920  fsumsplitf  11934  fsum2dlemstep  11960  fisumcom2  11964  fsumshftm  11971  fisum0diag2  11973  fsummulc2  11974  fsum00  11988  fsumabs  11991  fsumrelem  11997  fsumiun  12003  isumshft  12016  mertenslem2  12062  prodrbdclem  12097  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  prodfct  12113  prodssdc  12115  fprodmul  12117  fprodm1s  12127  fprodp1s  12128  fprodcl2lem  12131  fprodabs  12142  fprod2dlemstep  12148  fprodcom2fi  12152  fprodrec  12155  fproddivapf  12157  fprodsplitf  12158  fprodsplit1f  12160  fprodle  12166  pcmpt  12881  pcmptdvds  12883  gsumfzfsumlemm  14566  iuncld  14804  fsumcncntop  15256  dvmptfsum  15414