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  3275  uneq1  3310  ineq1  3357  nel02  3455  n0i  3456  disjel  3505  exsnrex  3664  sneqr  3790  preqr1g  3796  preqr1  3798  preq12b  3800  prel12  3801  elunii  3844  eluniab  3851  ssuni  3861  elinti  3883  elintab  3885  intss1  3889  intmin  3894  intab  3903  iineq2  3933  dfiin2g  3949  breq  4035  axsep2  4152  zfauscl  4153  inuni  4188  exmidexmid  4229  ss1o0el1  4230  exmid01  4231  exmidundif  4239  exmidundifim  4240  rext  4248  intid  4257  mss  4259  opth1  4269  opeqex  4282  frforeq3  4382  frirrg  4385  limeq  4412  nsuceq0g  4453  suctr  4456  snnex  4483  uniuni  4486  iunpw  4515  ordtriexmidlem  4555  ordtriexmidlem2  4556  ordtriexmid  4557  ontriexmidim  4558  ordtri2orexmid  4559  ontr2exmid  4561  ordtri2or2exmidlem  4562  onsucelsucexmidlem  4565  onsucelsucexmid  4566  ordsucunielexmid  4567  regexmidlem1  4569  reg2exmidlema  4570  regexmid  4571  reg2exmid  4572  elirr  4577  en2lp  4590  suc11g  4593  dtruex  4595  ordsoexmid  4598  nlimsucg  4602  onintexmid  4609  reg3exmidlemwe  4615  reg3exmid  4616  peano5  4634  limom  4650  0elnn  4655  nn0eln0  4656  nnregexmid  4657  xpeq1  4677  xpeq2  4678  opthprc  4714  xp11m  5108  funopg  5292  dffo4  5710  elunirn  5813  f1oiso  5873  canth  5875  eusvobj2  5908  acexmidlema  5913  acexmidlemb  5914  acexmidlemab  5916  acexmidlem2  5919  mpoeq123  5981  oprssdmm  6229  unielxp  6232  cnvf1o  6283  smoel  6358  tfr0dm  6380  frecabcl  6457  nnsucelsuc  6549  nntri3or  6551  nntri2  6552  nntri3  6555  nndceq  6557  nnmordi  6574  nnaordex  6586  elqsn0m  6662  qsel  6671  mapsn  6749  pw2f1odclem  6895  findcard2s  6951  undifdcss  6984  ctssdclemr  7178  nnnninf2  7193  exmidonfinlem  7260  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  exmidontriimlem3  7290  exmidontriimlem4  7291  exmidontriim  7292  pw1ne3  7297  sucpw1ne3  7299  sucpw1nel3  7300  onntri35  7304  elni2  7381  addnidpig  7403  elinp  7541  suplocexprlemdisj  7787  suplocexprlemub  7790  pitonn  7915  peano1nnnn  7919  peano2nnnn  7920  peano5nnnn  7959  sup3exmid  8984  peano5nni  8993  1nn  9001  peano2nn  9002  dfuzi  9436  uz11  9624  elfzonlteqm1  10286  frec2uzltd  10495  0tonninf  10532  1tonninf  10533  wrdsymb0  10967  sumeq1  11520  prodeq1f  11717  nninfctlemfo  12207  ctiunct  12657  ssomct  12662  issubm  13104  isnsg  13332  releqgg  13350  eqgex  13351  resghm  13390  ghmeql  13397  issubrg  13777  lmodfopnelem2  13881  islssm  13913  islssmg  13914  lspsneq0  13982  istopg  14235  fiinbas  14285  topbas  14303  epttop  14326  restbasg  14404  icnpimaex  14447  lmcvg  14453  iscnp4  14454  cncnpi  14464  cnconst2  14469  cnptoprest  14475  cnptoprest2  14476  cnpdis  14478  lmss  14482  lmff  14485  txbas  14494  eltx  14495  txcnp  14507  txlm  14515  blssps  14663  blss  14664  blssexps  14665  blssex  14666  neibl  14727  metss  14730  metrest  14742  xmettx  14746  metcnp3  14747  tgioo  14790  tgqioo  14791  bdsep2  15532  bdzfauscl  15536  bj-indeq  15575  bj-nn0suc0  15596  bj-nnelirr  15599  bj-peano4  15601  bj-inf2vnlem2  15617  bj-nn0sucALT  15624  bj-findis  15625  strcollnft  15630  sscoll2  15634  nninfsellemdc  15654  nninfsellemqall  15659