Theorem eleq1a 2834

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 2826	. 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2	1	biimprcd 249	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  elex2  3443  elex22  3444  disj  4378  disjne  4385  elpr2g  4582  eqoreldif  4617  ordelinel  6349  onun2  6355  ssimaex  6835  fnex  7075  f1ocnv2d  7500  peano5  7714  peano5OLD  7715  mpoexw  7892  tfrlem8  8186  tz7.48-2  8243  tz7.49  8246  eroprf  8562  pssnn  8913  onfin  8944  pssnnOLD  8969  ac6sfi  8988  elfiun  9119  brwdom  9256  ficardom  9650  ficard  10252  tskxpss  10459  inar1  10462  rankcf  10464  tskuni  10470  gruun  10493  nsmallnq  10664  prnmadd  10684  genpss  10691  eqlei  11015  eqlei2  11016  renegcli  11212  supaddc  11872  supadd  11873  supmul1  11874  supmullem2  11876  supmul  11877  nn0ind-raph  12350  uzwo  12580  iccid  13053  hashvnfin  14003  hashdifsnp1  14138  mertenslem2  15525  4sqlem1  16577  4sqlem4  16581  4sqlem11  16584  symggen  18993  psgnran  19038  odlem1  19058  gexlem1  19099  gsumpr  19471  lssvneln0  20128  lss1d  20140  lspsn  20179  lsmelval2  20262  psgnghm  20697  opnneiid  22185  cmpsublem  22458  metrest  23586  metustel  23612  dscopn  23635  ovolshftlem2  24579  subopnmbl  24673  deg1ldgn  25163  plyremlem  25369  coseq0negpitopi  25565  ppiublem1  26255  mptelee  27166  nbuhgr2vtx1edgblem  27621  numclwwlk1lem2foa  28619  shsleji  29633  spansnss  29834  spansncvi  29915  f1o3d  30863  sigaclcu2  31988  measdivcstALTV  32093  dfon2lem6  33670  noextendseq  33797  bdayfo  33807  scutf  33933  altxpsspw  34206  hfun  34407  ontgval  34547  ordtoplem  34551  ordcmp  34563  findreccl  34569  bj-xpnzex  35076  bj-snsetex  35080  bj-ismooredr2  35208  bj-ideqg1  35262  topdifinfindis  35444  finxpreclem1  35487  ovoliunnfl  35746  volsupnfl  35749  heibor1lem  35894  heibor1  35895  lshpkrlem1  37051  lfl1dim  37062  leat3  37236  meetat2  37238  glbconxN  37319  pointpsubN  37692  pmapglbx  37710  linepsubclN  37892  dia2dimlem7  39011  dib1dim2  39109  diclspsn  39135  dih1dimatlem  39270  dihatexv2  39280  djhlsmcl  39355  fsuppssind  40205  fltne  40397  3cubes  40428  hbtlem2  40865  hbtlem5  40869  rp-isfinite6  41023  snssiALTVD  42336  snssiALT  42337  elex2VD  42347  elex22VD  42348  fveqvfvv  44421  afv0fv0  44528  lswn0  44784  lidlmmgm  45371  1neven  45378  cznrng  45401