Theorem eleq1a 2860

Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
eleq1a	⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem eleq1a

Step	Hyp	Ref	Expression
1		eleq1 2853	. 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2	1	biimprcd 253	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  elex22  3481  disjne  4415  rabsneq  4610  elpr2g  4617  eqoreldif  4653  ordelinel  6468  onun2  6475  ssimaex  6970  fnex  7219  f1ocnv2d  7669  omun  7886  peano5  7892  mpoexw  8077  tfrlem8  8373  tz7.48-2  8431  tz7.49  8434  eroprf  8815  pssnn  9156  onfin  9202  ac6sfi  9247  elfiun  9393  brwdom  9532  ficardom  9959  ficard  10560  tskxpss  10768  inar1  10771  rankcf  10773  tskuni  10779  gruun  10802  nsmallnq  10973  prnmadd  10993  genpss  11000  mpoaddf  11205  mpomulf  11206  eqlei  11331  eqlei2  11332  renegcli  11530  supaddc  12193  supadd  12194  supmul1  12195  supmullem2  12197  supmul  12198  nn0ind-raph  12707  uzwo  12946  iccid  13428  hashvnfin  14409  hashdifsnp1  14556  mertenslem2  15957  4sqlem1  17025  4sqlem4  17029  4sqlem11  17032  symggen  19563  psgnran  19608  odlem1  19628  gexlem1  19672  gsumpr  20048  lssvneln0  21102  lss1d  21113  lspsn  21152  lsmelval2  21235  rnglidlmmgm  21408  psgnghm  21759  opnneiid  23312  cmpsublem  23585  metrest  24710  metustel  24736  dscopn  24759  ovolshftlem2  25698  subopnmbl  25792  deg1ldgn  26279  plyremlem  26494  coseq0negpitopi  26697  ppiublem1  27395  noextendseq  27860  bdayfo  27870  cutsf  28014  addsproplem2  28192  mpteleeOLD  29274  nbuhgr2vtx1edgblem  29730  numclwwlk1lem2foa  30734  shsleji  31751  spansnss  31952  spansncvi  32033  f1o3d  33000  sigaclcu2  34533  measdivcstALTV  34639  kardfi  35599  dfon2lem6  36291  altxpsspw  36482  hfun  36683  ontgval  36975  ordtoplem  36979  ordcmp  36991  findreccl  36997  bj-xpnzex  37628  bj-snsetex  37632  bj-ismooredr2  37785  bj-ideqg1  37841  topdifinfindis  38025  finxpreclem1  38068  ovoliunnfl  38346  volsupnfl  38349  heibor1lem  38493  heibor1  38494  lshpkrlem1  39917  lfl1dim  39928  leat3  40102  meetat2  40104  glbconxN  40185  pointpsubN  40558  pmapglbx  40576  linepsubclN  40758  dia2dimlem7  41877  dib1dim2  41975  diclspsn  42001  dih1dimatlem  42136  dihatexv2  42146  djhlsmcl  42221  fsuppssind  43358  fltne  43409  3cubes  43454  hbtlem2  43884  hbtlem5  43888  rp-isfinite6  44277  snssiALTVD  45568  snssiALT  45569  elex2VD  45579  elex22VD  45580  fveqvfvv  47810  afv0fv0  47919  lswn0  48226  1neven  49036  cznrng  49059