Theorem eleq2 2260

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 2190	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1572	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	anbi2d 464	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	exbidv 1839	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2192	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2192	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  eleq12  2261  eleq2i  2263  eleq2d  2266  nelneq2  2298  clelsb2  2302  dvelimdc  2360  nelne1  2457  neleq2  2467  raleqf  2689  rexeqf  2690  reueq1f  2691  rmoeq1f  2692  rabeqf  2753  clel3g  2898  clel4  2900  sbcbi2  3040  sbcel2gv  3053  csbeq2  3108  sbnfc2  3145  difeq2  3276  uneq1  3311  ineq1  3358  nel02  3456  n0i  3457  disjel  3506  exsnrex  3665  sneqr  3791  preqr1g  3797  preqr1  3799  preq12b  3801  prel12  3802  elunii  3845  eluniab  3852  ssuni  3862  elinti  3884  elintab  3886  intss1  3890  intmin  3895  intab  3904  iineq2  3934  dfiin2g  3950  breq  4036  axsep2  4153  zfauscl  4154  inuni  4189  exmidexmid  4230  ss1o0el1  4231  exmid01  4232  exmidundif  4240  exmidundifim  4241  rext  4249  intid  4258  mss  4260  opth1  4270  opeqex  4283  frforeq3  4383  frirrg  4386  limeq  4413  nsuceq0g  4454  suctr  4457  snnex  4484  uniuni  4487  iunpw  4516  ordtriexmidlem  4556  ordtriexmidlem2  4557  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  ontr2exmid  4562  ordtri2or2exmidlem  4563  onsucelsucexmidlem  4566  onsucelsucexmid  4567  ordsucunielexmid  4568  regexmidlem1  4570  reg2exmidlema  4571  regexmid  4572  reg2exmid  4573  elirr  4578  en2lp  4591  suc11g  4594  dtruex  4596  ordsoexmid  4599  nlimsucg  4603  onintexmid  4610  reg3exmidlemwe  4616  reg3exmid  4617  peano5  4635  limom  4651  0elnn  4656  nn0eln0  4657  nnregexmid  4658  xpeq1  4678  xpeq2  4679  opthprc  4715  xp11m  5109  funopg  5293  dffo4  5713  elunirn  5816  f1oiso  5876  canth  5878  eusvobj2  5911  acexmidlema  5916  acexmidlemb  5917  acexmidlemab  5919  acexmidlem2  5922  mpoeq123  5985  oprssdmm  6238  unielxp  6241  cnvf1o  6292  smoel  6367  tfr0dm  6389  frecabcl  6466  nnsucelsuc  6558  nntri3or  6560  nntri2  6561  nntri3  6564  nndceq  6566  nnmordi  6583  nnaordex  6595  elqsn0m  6671  qsel  6680  mapsn  6758  pw2f1odclem  6904  findcard2s  6960  undifdcss  6993  ctssdclemr  7187  nnnninf2  7202  exmidonfinlem  7272  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  finacn  7287  exmidaclem  7291  exmidontriimlem3  7306  exmidontriimlem4  7307  exmidontriim  7308  pw1ne3  7313  sucpw1ne3  7315  sucpw1nel3  7316  onntri35  7320  acnccim  7355  elni2  7398  addnidpig  7420  elinp  7558  suplocexprlemdisj  7804  suplocexprlemub  7807  pitonn  7932  peano1nnnn  7936  peano2nnnn  7937  peano5nnnn  7976  sup3exmid  9001  peano5nni  9010  1nn  9018  peano2nn  9019  dfuzi  9453  uz11  9641  elfzonlteqm1  10303  frec2uzltd  10512  0tonninf  10549  1tonninf  10550  wrdsymb0  10984  sumeq1  11537  prodeq1f  11734  nninfctlemfo  12232  ctiunct  12682  ssomct  12687  issubm  13174  isnsg  13408  releqgg  13426  eqgex  13427  resghm  13466  ghmeql  13473  issubrg  13853  lmodfopnelem2  13957  islssm  13989  islssmg  13990  lspsneq0  14058  istopg  14319  fiinbas  14369  topbas  14387  epttop  14410  restbasg  14488  icnpimaex  14531  lmcvg  14537  iscnp4  14538  cncnpi  14548  cnconst2  14553  cnptoprest  14559  cnptoprest2  14560  cnpdis  14562  lmss  14566  lmff  14569  txbas  14578  eltx  14579  txcnp  14591  txlm  14599  blssps  14747  blss  14748  blssexps  14749  blssex  14750  neibl  14811  metss  14814  metrest  14826  xmettx  14830  metcnp3  14831  tgioo  14874  tgqioo  14875  bdsep2  15616  bdzfauscl  15620  bj-indeq  15659  bj-nn0suc0  15680  bj-nnelirr  15683  bj-peano4  15685  bj-inf2vnlem2  15701  bj-nn0sucALT  15708  bj-findis  15709  strcollnft  15714  sscoll2  15718  2omap  15726  nninfsellemdc  15741  nninfsellemqall  15746