Theorem nfel1 2360

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

Syntax hints:  Ⅎwnf 1484   ∈ wcel 2177  Ⅎwnfc 2336

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-cleq 2199  df-clel 2202  df-nfc 2338

This theorem is referenced by:  vtocl2gf  2837  vtocl3gf  2838  vtoclgaf  2840  vtocl2gaf  2842  vtocl3gaf  2844  nfop  3844  pofun  4372  nfse  4401  rabxfrd  4529  mptfvex  5683  fvmptf  5690  fmptcof  5765  fliftfuns  5885  riota2f  5939  ovmpos  6087  ov2gf  6088  elovmporab  6164  elovmporab1w  6165  fmpox  6304  mpofvex  6309  qliftfuns  6724  xpf1o  6961  iunfidisj  7069  cc3  7410  infssuzcldc  10410  sumfct  11770  sumrbdclem  11773  summodclem3  11776  summodclem2a  11777  zsumdc  11780  fsumgcl  11782  fsum3  11783  isumss  11787  isumss2  11789  fsum3cvg2  11790  fsumsplitf  11804  fsum2dlemstep  11830  fisumcom2  11834  fsumshftm  11841  fisum0diag2  11843  fsummulc2  11844  fsum00  11858  fsumabs  11861  fsumrelem  11867  fsumiun  11873  isumshft  11886  mertenslem2  11932  prodrbdclem  11967  prodmodclem3  11971  prodmodclem2a  11972  zproddc  11975  fprodseq  11979  prodfct  11983  prodssdc  11985  fprodmul  11987  fprodm1s  11997  fprodp1s  11998  fprodcl2lem  12001  fprodabs  12012  fprod2dlemstep  12018  fprodcom2fi  12022  fprodrec  12025  fproddivapf  12027  fprodsplitf  12028  fprodsplit1f  12030  fprodle  12036  pcmpt  12751  pcmptdvds  12753  gsumfzfsumlemm  14434  iuncld  14672  fsumcncntop  15124  dvmptfsum  15282