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  2800  vtocl3gf  2801  vtoclgaf  2803  vtocl2gaf  2805  vtocl3gaf  2807  nfop  3795  pofun  4313  nfse  4342  rabxfrd  4470  mptfvex  5602  fvmptf  5609  fmptcof  5684  fliftfuns  5799  riota2f  5852  ovmpos  5998  ov2gf  5999  fmpox  6201  mpofvex  6204  qliftfuns  6619  xpf1o  6844  iunfidisj  6945  cc3  7267  sumfct  11382  sumrbdclem  11385  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsumgcl  11394  fsum3  11395  isumss  11399  isumss2  11401  fsum3cvg2  11402  fsumsplitf  11416  fsum2dlemstep  11442  fisumcom2  11446  fsumshftm  11453  fisum0diag2  11455  fsummulc2  11456  fsum00  11470  fsumabs  11473  fsumrelem  11479  fsumiun  11485  isumshft  11498  mertenslem2  11544  prodrbdclem  11579  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  prodfct  11595  prodssdc  11597  fprodmul  11599  fprodm1s  11609  fprodp1s  11610  fprodcl2lem  11613  fprodabs  11624  fprod2dlemstep  11630  fprodcom2fi  11634  fprodrec  11637  fproddivapf  11639  fprodsplitf  11640  fprodsplit1f  11642  fprodle  11648  infssuzcldc  11952  pcmpt  12341  pcmptdvds  12343  iuncld  13618  fsumcncntop  14059