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  3794  pofun  4311  nfse  4340  rabxfrd  4468  mptfvex  5600  fvmptf  5607  fmptcof  5682  fliftfuns  5796  riota2f  5849  ovmpos  5995  ov2gf  5996  fmpox  6198  mpofvex  6201  qliftfuns  6616  xpf1o  6841  iunfidisj  6942  cc3  7264  sumfct  11375  sumrbdclem  11378  summodclem3  11381  summodclem2a  11382  zsumdc  11385  fsumgcl  11387  fsum3  11388  isumss  11392  isumss2  11394  fsum3cvg2  11395  fsumsplitf  11409  fsum2dlemstep  11435  fisumcom2  11439  fsumshftm  11446  fisum0diag2  11448  fsummulc2  11449  fsum00  11463  fsumabs  11466  fsumrelem  11472  fsumiun  11478  isumshft  11491  mertenslem2  11537  prodrbdclem  11572  prodmodclem3  11576  prodmodclem2a  11577  zproddc  11580  fprodseq  11584  prodfct  11588  prodssdc  11590  fprodmul  11592  fprodm1s  11602  fprodp1s  11603  fprodcl2lem  11606  fprodabs  11617  fprod2dlemstep  11623  fprodcom2fi  11627  fprodrec  11630  fproddivapf  11632  fprodsplitf  11633  fprodsplit1f  11635  fprodle  11641  infssuzcldc  11944  pcmpt  12333  pcmptdvds  12335  iuncld  13486  fsumcncntop  13927