Theorem eleq1a 2855

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  elex22  3474  disjne  4407  rabsneq  4599  elpr2g  4606  eqoreldif  4642  ordelinel  6466  onun2  6473  ssimaex  6971  fnex  7224  f1ocnv2d  7675  omun  7900  peano5  7906  mpoexw  8092  tfrlem8  8396  tz7.48-2  8456  tz7.49  8459  eroprf  8840  pssnn  9188  onfin  9234  ac6sfi  9279  elfiun  9426  brwdom  9565  hfunOLD  9923  ficardom  10046  ficard  10653  tskxpss  10861  inar1  10864  rankcf  10866  tskuni  10872  gruun  10895  nsmallnq  11066  prnmadd  11086  genpss  11093  mpoaddf  11298  mpomulf  11299  eqlei  11424  eqlei2  11425  renegcli  11623  supaddc  12288  supadd  12289  supmul1  12290  supmullem2  12292  supmul  12293  nn0ind-raph  12803  uzwo  13042  iccid  13525  hashvnfin  14508  hashdifsnp1  14655  mertenslem2  16060  4sqlem1  17132  4sqlem4  17136  4sqlem11  17139  symggen  19690  psgnran  19735  odlem1  19755  gexlem1  19799  gsumpr  20175  lssvneln0  21233  lss1d  21244  lspsn  21283  lsmelval2  21366  rnglidlmmgm  21539  psgnghm  21892  opnneiid  23450  cmpsublem  23723  metrest  24849  metustel  24875  dscopn  24898  ovolshftlem2  25837  subopnmbl  25931  deg1ldgn  26417  plyremlem  26631  coseq0negpitopi  26838  ppiublem1  27535  fltne  27981  noextendseq  28030  bdayfo  28040  cutsf  28184  addsproplem2  28362  mpteleeOLD  29479  nbuhgr2vtx1edgblem  29938  numclwwlk1lem2foa  30961  shsleji  31978  spansnss  32179  spansncvi  32260  f1o3d  33268  sigaclcu2  34799  measdivcstALTV  34905  kardfi  35895  dfon2lem6  36643  altxpsspw  36835  ontgval  37312  ordtoplem  37316  ordcmp  37328  findreccl  37334  bj-xpnzex  37965  bj-snsetex  37969  bj-ismooredr2  38124  bj-ideqg1  38179  topdifinfindis  38363  finxpreclem1  38406  ovoliunnfl  38674  volsupnfl  38677  heibor1lem  38837  heibor1  38838  lshpkrlem1  40261  lfl1dim  40272  leat3  40446  meetat2  40448  glbconxN  40529  pointpsubN  40902  pmapglbx  40920  linepsubclN  41102  dia2dimlem7  42221  dib1dim2  42319  diclspsn  42345  dih1dimatlem  42480  dihatexv2  42490  djhlsmcl  42565  fsuppssind  43715  3cubes  43794  hbtlem2  44220  hbtlem5  44224  rp-isfinite6  44613  snssiALTVD  45903  snssiALT  45904  elex2VD  45914  elex22VD  45915  fveqvfvv  48204  afv0fv0  48313  lswn0  48620  1neven  49429  cznrng  49452