Theorem eleq2 1150

Description: Equality implies equivalence of membership.

Assertion

Ref	Expression
eleq2	⊢ (A = B → (C ∈ A ↔ C ∈ B))

Proof of Theorem eleq2

Step	Hyp	Ref	Expression
1		dfcleq 1098	. . . . . 6 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
2	1	biimp 133	. . . . 5 ⊢ (A = B → ∀x(x ∈ A ↔ x ∈ B))
3	2	19.21bi 742	. . . 4 ⊢ (A = B → (x ∈ A ↔ x ∈ B))
4	3	anbi2d 468	. . 3 ⊢ (A = B → ((x = C ∧ x ∈ A) ↔ (x = C ∧ x ∈ B)))
5	4	biexdv 936	. 2 ⊢ (A = B → (∃x(x = C ∧ x ∈ A) ↔ ∃x(x = C ∧ x ∈ B)))
6		df-clel 1099	. 2 ⊢ (C ∈ A ↔ ∃x(x = C ∧ x ∈ A))
7		df-clel 1099	. 2 ⊢ (C ∈ B ↔ ∃x(x = C ∧ x ∈ B))
8	5, 6, 7	3bitr4g 428	1 ⊢ (A = B → (C ∈ A ↔ C ∈ B))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  eleq12 1151  eleq2i 1153  eleq2d 1156  clneq2 1169  neleq2 1200  raleqf 1321  rexeqf 1322  reueqf 1323  rabeqf 1345  clel3 1375  clel4 1376  sbcel2 1467  axrep 1473  zfrepclf 1477  difeq1 1582  difeq2 1583  uneq1 1605  ineq1 1638  unineq 1680  n0i 1712  rzal 1773  ifeq1 1778  ifeq2 1779  disjsn 1836  sneqr 1856  el 1860  rext 1862  preqr1 1872  preq12b 1874  prel12 1875  opth 1898  opprc3 1908  opthwiener 1914  elunii 1924  eluniab 1926  unieq 1927  euuni 1954  reucl 1957  unipw 1960  elinti 1974  elintab 1976  intss1 1979  intmin 1982  iineq2 2007  iununi 2037  iunpw 2040  trel 2048  breq 2064  epelc 2123  efrirr 2180  ordtri1 2231  ordtri3 2234  oneqmin 2273  onminex 2275  nsuceq0 2306  ordnbtwn 2316  onuninsuc 2356  limsuc 2361  limomss 2378  nnlim 2385  peano5 2394  xpeq1 2440  xpeq2 2441  opelxpex 2445  opthprc 2457  0nelxp 2475  onxpdisj 2476  fn0 2739  fv3 2839  f1oiso 2942  canth 2945  tz7.48lem 2993  oawordeulem 3156  oaordex 3160  omordi 3164  omsmolem 3195  erth 3219  mapsn 3269  pw2en 3348  pssnn 3428  unfilem3 3440  zfregcl 3446  eirr 3450  en2lp 3453  suc11reg 3456  inf0 3457  inf3lem2 3465  inf3lem3 3466  inf5 3472  inf4 3473  dfom3 3477  elom3 3478  r1ord 3499  r1val1 3502  rankr1 3518  rankval3 3525  rankuni 3533  rankun 3535  aceq1 3552  aceq2 3554  aceq3 3556  aceq5lem2 3559  aceq5lem4 3561  aceq6a 3564  aceq6b 3565  kmlem2 3581  kmlem4 3583  zornlem7 3609  cardlim 3657  alephnbtwn 3674  alephordi 3679  cardaleph 3690  axpowndlem3 3745  ltpiord 3809  addnidpi 3822  indpi 3828  elnp 3886  genpnnp 3902  1pr 3911  ltaddpr 3934  peano5nn 4424  om2uzlt 4654  sh 5116  closedsub 5128  pjthut 5243  pjmvalt 5245  pjoc1t 5270  pjoml 5271  h1dn0 5457  spansneleqi 5474  pjcht 5582  pjnelt 5667

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org