Theorem eleq2 2270

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1371   = wceq 1373  ∃wex 1516   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eleq12  2271  eleq2i  2273  eleq2d  2276  nelneq2  2308  clelsb2  2312  dvelimdc  2370  nelne1  2467  neleq2  2477  raleqf  2699  rexeqf  2700  reueq1f  2701  rmoeq1f  2702  rabeqf  2763  clel3g  2911  clel4  2913  sbcbi2  3053  sbcel2gv  3066  csbeq2  3121  sbnfc2  3158  difeq2  3289  uneq1  3324  ineq1  3371  nel02  3469  n0i  3470  disjel  3519  exsnrex  3680  sneqr  3807  preqr1g  3813  preqr1  3815  preq12b  3817  prel12  3818  elunii  3861  eluniab  3868  ssuni  3878  elinti  3900  elintab  3902  intss1  3906  intmin  3911  intab  3920  iineq2  3950  dfiin2g  3966  breq  4053  axsep2  4171  zfauscl  4172  inuni  4207  exmidexmid  4248  ss1o0el1  4249  exmid01  4250  exmidundif  4258  exmidundifim  4259  rext  4267  intid  4276  mss  4278  opth1  4288  opeqex  4302  frforeq3  4402  frirrg  4405  limeq  4432  nsuceq0g  4473  suctr  4476  snnex  4503  uniuni  4506  iunpw  4535  ordtriexmidlem  4575  ordtriexmidlem2  4576  ordtriexmid  4577  ontriexmidim  4578  ordtri2orexmid  4579  ontr2exmid  4581  ordtri2or2exmidlem  4582  onsucelsucexmidlem  4585  onsucelsucexmid  4586  ordsucunielexmid  4587  regexmidlem1  4589  reg2exmidlema  4590  regexmid  4591  reg2exmid  4592  elirr  4597  en2lp  4610  suc11g  4613  dtruex  4615  ordsoexmid  4618  nlimsucg  4622  onintexmid  4629  reg3exmidlemwe  4635  reg3exmid  4636  peano5  4654  limom  4670  0elnn  4675  nn0eln0  4676  nnregexmid  4677  xpeq1  4697  xpeq2  4698  opthprc  4734  xp11m  5130  funopg  5314  dffo4  5741  funopdmsn  5777  elunirn  5848  f1oiso  5908  canth  5910  eusvobj2  5943  acexmidlema  5948  acexmidlemb  5949  acexmidlemab  5951  acexmidlem2  5954  mpoeq123  6017  oprssdmm  6270  unielxp  6273  cnvf1o  6324  smoel  6399  tfr0dm  6421  frecabcl  6498  nnsucelsuc  6590  nntri3or  6592  nntri2  6593  nntri3  6596  nndceq  6598  nnmordi  6615  nnaordex  6627  elqsn0m  6703  qsel  6712  mapsn  6790  en2m  6927  pw2f1odclem  6946  findcard2s  7002  undifdcss  7035  ctssdclemr  7229  nnnninf2  7244  exmidonfinlem  7317  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  finacn  7332  exmidaclem  7336  exmidontriimlem3  7351  exmidontriimlem4  7352  exmidontriim  7353  iftrueb01  7354  pw1ne3  7361  sucpw1ne3  7363  sucpw1nel3  7364  onntri35  7368  acnccim  7404  elni2  7447  addnidpig  7469  elinp  7607  suplocexprlemdisj  7853  suplocexprlemub  7856  pitonn  7981  peano1nnnn  7985  peano2nnnn  7986  peano5nnnn  8025  sup3exmid  9050  peano5nni  9059  1nn  9067  peano2nn  9068  dfuzi  9503  uz11  9691  elfzonlteqm1  10361  frec2uzltd  10570  0tonninf  10607  1tonninf  10608  wrdsymb0  11048  lsw0  11063  swrdwrdsymbg  11140  sumeq1  11741  prodeq1f  11938  nninfctlemfo  12436  ctiunct  12886  ssomct  12891  issubm  13379  isnsg  13613  releqgg  13631  eqgex  13632  resghm  13671  ghmeql  13678  issubrg  14058  lmodfopnelem2  14162  islssm  14194  islssmg  14195  lspsneq0  14263  istopg  14546  fiinbas  14596  topbas  14614  epttop  14637  restbasg  14715  icnpimaex  14758  lmcvg  14764  iscnp4  14765  cncnpi  14775  cnconst2  14780  cnptoprest  14786  cnptoprest2  14787  cnpdis  14789  lmss  14793  lmff  14796  txbas  14805  eltx  14806  txcnp  14818  txlm  14826  blssps  14974  blss  14975  blssexps  14976  blssex  14977  neibl  15038  metss  15041  metrest  15053  xmettx  15057  metcnp3  15058  tgioo  15101  tgqioo  15102  uhgrm  15749  lpvtx  15750  incistruhgr  15761  umgrnloopvv  15785  bdsep2  15960  bdzfauscl  15964  bj-indeq  16003  bj-nn0suc0  16024  bj-nnelirr  16027  bj-peano4  16029  bj-inf2vnlem2  16045  bj-nn0sucALT  16052  bj-findis  16053  strcollnft  16058  sscoll2  16062  2omap  16071  nninfsellemdc  16088  nninfsellemqall  16093  nnnninfex  16100