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  2895  clel4  2897  sbcbi2  3037  sbcel2gv  3050  csbeq2  3105  sbnfc2  3142  difeq2  3272  uneq1  3307  ineq1  3354  nel02  3452  n0i  3453  disjel  3502  exsnrex  3661  sneqr  3787  preqr1g  3793  preqr1  3795  preq12b  3797  prel12  3798  elunii  3841  eluniab  3848  ssuni  3858  elinti  3880  elintab  3882  intss1  3886  intmin  3891  intab  3900  iineq2  3930  dfiin2g  3946  breq  4032  axsep2  4149  zfauscl  4150  inuni  4185  exmidexmid  4226  ss1o0el1  4227  exmid01  4228  exmidundif  4236  exmidundifim  4237  rext  4245  intid  4254  mss  4256  opth1  4266  opeqex  4279  frforeq3  4379  frirrg  4382  limeq  4409  nsuceq0g  4450  suctr  4453  snnex  4480  uniuni  4483  iunpw  4512  ordtriexmidlem  4552  ordtriexmidlem2  4553  ordtriexmid  4554  ontriexmidim  4555  ordtri2orexmid  4556  ontr2exmid  4558  ordtri2or2exmidlem  4559  onsucelsucexmidlem  4562  onsucelsucexmid  4563  ordsucunielexmid  4564  regexmidlem1  4566  reg2exmidlema  4567  regexmid  4568  reg2exmid  4569  elirr  4574  en2lp  4587  suc11g  4590  dtruex  4592  ordsoexmid  4595  nlimsucg  4599  onintexmid  4606  reg3exmidlemwe  4612  reg3exmid  4613  peano5  4631  limom  4647  0elnn  4652  nn0eln0  4653  nnregexmid  4654  xpeq1  4674  xpeq2  4675  opthprc  4711  xp11m  5105  funopg  5289  dffo4  5707  elunirn  5810  f1oiso  5870  canth  5872  eusvobj2  5905  acexmidlema  5910  acexmidlemb  5911  acexmidlemab  5913  acexmidlem2  5916  mpoeq123  5978  oprssdmm  6226  unielxp  6229  cnvf1o  6280  smoel  6355  tfr0dm  6377  frecabcl  6454  nnsucelsuc  6546  nntri3or  6548  nntri2  6549  nntri3  6552  nndceq  6554  nnmordi  6571  nnaordex  6583  elqsn0m  6659  qsel  6668  mapsn  6746  pw2f1odclem  6892  findcard2s  6948  undifdcss  6981  ctssdclemr  7173  nnnninf2  7188  exmidonfinlem  7255  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  exmidontriimlem3  7285  exmidontriimlem4  7286  exmidontriim  7287  pw1ne3  7292  sucpw1ne3  7294  sucpw1nel3  7295  onntri35  7299  elni2  7376  addnidpig  7398  elinp  7536  suplocexprlemdisj  7782  suplocexprlemub  7785  pitonn  7910  peano1nnnn  7914  peano2nnnn  7915  peano5nnnn  7954  sup3exmid  8978  peano5nni  8987  1nn  8995  peano2nn  8996  dfuzi  9430  uz11  9618  elfzonlteqm1  10280  frec2uzltd  10477  0tonninf  10514  1tonninf  10515  wrdsymb0  10949  sumeq1  11501  prodeq1f  11698  nninfctlemfo  12180  ctiunct  12600  ssomct  12605  issubm  13047  isnsg  13275  releqgg  13293  eqgex  13294  resghm  13333  ghmeql  13340  issubrg  13720  lmodfopnelem2  13824  islssm  13856  islssmg  13857  lspsneq0  13925  istopg  14178  fiinbas  14228  topbas  14246  epttop  14269  restbasg  14347  icnpimaex  14390  lmcvg  14396  iscnp4  14397  cncnpi  14407  cnconst2  14412  cnptoprest  14418  cnptoprest2  14419  cnpdis  14421  lmss  14425  lmff  14428  txbas  14437  eltx  14438  txcnp  14450  txlm  14458  blssps  14606  blss  14607  blssexps  14608  blssex  14609  neibl  14670  metss  14673  metrest  14685  xmettx  14689  metcnp3  14690  tgioo  14733  tgqioo  14734  bdsep2  15448  bdzfauscl  15452  bj-indeq  15491  bj-nn0suc0  15512  bj-nnelirr  15515  bj-peano4  15517  bj-inf2vnlem2  15533  bj-nn0sucALT  15540  bj-findis  15541  strcollnft  15546  sscoll2  15550  nninfsellemdc  15570  nninfsellemqall  15575