Theorem nfel1 2358

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

Syntax hints:  Ⅎwnf 1482   ∈ wcel 2175  Ⅎwnfc 2334

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-cleq 2197  df-clel 2200  df-nfc 2336

This theorem is referenced by:  vtocl2gf  2834  vtocl3gf  2835  vtoclgaf  2837  vtocl2gaf  2839  vtocl3gaf  2841  nfop  3834  pofun  4358  nfse  4387  rabxfrd  4515  mptfvex  5664  fvmptf  5671  fmptcof  5746  fliftfuns  5866  riota2f  5920  ovmpos  6068  ov2gf  6069  elovmporab  6145  elovmporab1w  6146  fmpox  6285  mpofvex  6290  qliftfuns  6705  xpf1o  6940  iunfidisj  7047  cc3  7379  infssuzcldc  10376  sumfct  11627  sumrbdclem  11630  summodclem3  11633  summodclem2a  11634  zsumdc  11637  fsumgcl  11639  fsum3  11640  isumss  11644  isumss2  11646  fsum3cvg2  11647  fsumsplitf  11661  fsum2dlemstep  11687  fisumcom2  11691  fsumshftm  11698  fisum0diag2  11700  fsummulc2  11701  fsum00  11715  fsumabs  11718  fsumrelem  11724  fsumiun  11730  isumshft  11743  mertenslem2  11789  prodrbdclem  11824  prodmodclem3  11828  prodmodclem2a  11829  zproddc  11832  fprodseq  11836  prodfct  11840  prodssdc  11842  fprodmul  11844  fprodm1s  11854  fprodp1s  11855  fprodcl2lem  11858  fprodabs  11869  fprod2dlemstep  11875  fprodcom2fi  11879  fprodrec  11882  fproddivapf  11884  fprodsplitf  11885  fprodsplit1f  11887  fprodle  11893  pcmpt  12608  pcmptdvds  12610  gsumfzfsumlemm  14291  iuncld  14529  fsumcncntop  14981  dvmptfsum  15139