Theorem eleq2 2257

Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eleq2	⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Proof of Theorem eleq2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2187	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1569	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	anbi2d 464	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	exbidv 1836	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2189	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2189	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2164

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-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  eleq12  2258  eleq2i  2260  eleq2d  2263  nelneq2  2295  clelsb2  2299  dvelimdc  2357  nelne1  2454  neleq2  2464  raleqf  2686  rexeqf  2687  reueq1f  2688  rmoeq1f  2689  rabeqf  2750  clel3g  2894  clel4  2896  sbcbi2  3036  sbcel2gv  3049  csbeq2  3104  sbnfc2  3141  difeq2  3271  uneq1  3306  ineq1  3353  nel02  3451  n0i  3452  disjel  3501  exsnrex  3660  sneqr  3786  preqr1g  3792  preqr1  3794  preq12b  3796  prel12  3797  elunii  3840  eluniab  3847  ssuni  3857  elinti  3879  elintab  3881  intss1  3885  intmin  3890  intab  3899  iineq2  3929  dfiin2g  3945  breq  4031  axsep2  4148  zfauscl  4149  inuni  4184  exmidexmid  4225  ss1o0el1  4226  exmid01  4227  exmidundif  4235  exmidundifim  4236  rext  4244  intid  4253  mss  4255  opth1  4265  opeqex  4278  frforeq3  4378  frirrg  4381  limeq  4408  nsuceq0g  4449  suctr  4452  snnex  4479  uniuni  4482  iunpw  4511  ordtriexmidlem  4551  ordtriexmidlem2  4552  ordtriexmid  4553  ontriexmidim  4554  ordtri2orexmid  4555  ontr2exmid  4557  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  onsucelsucexmid  4562  ordsucunielexmid  4563  regexmidlem1  4565  reg2exmidlema  4566  regexmid  4567  reg2exmid  4568  elirr  4573  en2lp  4586  suc11g  4589  dtruex  4591  ordsoexmid  4594  nlimsucg  4598  onintexmid  4605  reg3exmidlemwe  4611  reg3exmid  4612  peano5  4630  limom  4646  0elnn  4651  nn0eln0  4652  nnregexmid  4653  xpeq1  4673  xpeq2  4674  opthprc  4710  xp11m  5104  funopg  5288  dffo4  5706  elunirn  5809  f1oiso  5869  canth  5871  eusvobj2  5904  acexmidlema  5909  acexmidlemb  5910  acexmidlemab  5912  acexmidlem2  5915  mpoeq123  5977  oprssdmm  6224  unielxp  6227  cnvf1o  6278  smoel  6353  tfr0dm  6375  frecabcl  6452  nnsucelsuc  6544  nntri3or  6546  nntri2  6547  nntri3  6550  nndceq  6552  nnmordi  6569  nnaordex  6581  elqsn0m  6657  qsel  6666  mapsn  6744  pw2f1odclem  6890  findcard2s  6946  undifdcss  6979  ctssdclemr  7171  nnnninf2  7186  exmidonfinlem  7253  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  exmidontriimlem3  7283  exmidontriimlem4  7284  exmidontriim  7285  pw1ne3  7290  sucpw1ne3  7292  sucpw1nel3  7293  onntri35  7297  elni2  7374  addnidpig  7396  elinp  7534  suplocexprlemdisj  7780  suplocexprlemub  7783  pitonn  7908  peano1nnnn  7912  peano2nnnn  7913  peano5nnnn  7952  sup3exmid  8976  peano5nni  8985  1nn  8993  peano2nn  8994  dfuzi  9427  uz11  9615  elfzonlteqm1  10277  frec2uzltd  10474  0tonninf  10511  1tonninf  10512  wrdsymb0  10946  sumeq1  11498  prodeq1f  11695  nninfctlemfo  12177  ctiunct  12597  ssomct  12602  issubm  13044  isnsg  13272  releqgg  13290  eqgex  13291  resghm  13330  ghmeql  13337  issubrg  13717  lmodfopnelem2  13821  islssm  13853  islssmg  13854  lspsneq0  13922  istopg  14167  fiinbas  14217  topbas  14235  epttop  14258  restbasg  14336  icnpimaex  14379  lmcvg  14385  iscnp4  14386  cncnpi  14396  cnconst2  14401  cnptoprest  14407  cnptoprest2  14408  cnpdis  14410  lmss  14414  lmff  14417  txbas  14426  eltx  14427  txcnp  14439  txlm  14447  blssps  14595  blss  14596  blssexps  14597  blssex  14598  neibl  14659  metss  14662  metrest  14674  xmettx  14678  metcnp3  14679  tgioo  14714  tgqioo  14715  bdsep2  15378  bdzfauscl  15382  bj-indeq  15421  bj-nn0suc0  15442  bj-nnelirr  15445  bj-peano4  15447  bj-inf2vnlem2  15463  bj-nn0sucALT  15470  bj-findis  15471  strcollnft  15476  sscoll2  15480  nninfsellemdc  15500  nninfsellemqall  15505