Theorem eleq2 2268

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1370   = wceq 1372  ∃wex 1514   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  eleq12  2269  eleq2i  2271  eleq2d  2274  nelneq2  2306  clelsb2  2310  dvelimdc  2368  nelne1  2465  neleq2  2475  raleqf  2697  rexeqf  2698  reueq1f  2699  rmoeq1f  2700  rabeqf  2761  clel3g  2906  clel4  2908  sbcbi2  3048  sbcel2gv  3061  csbeq2  3116  sbnfc2  3153  difeq2  3284  uneq1  3319  ineq1  3366  nel02  3464  n0i  3465  disjel  3514  exsnrex  3674  sneqr  3800  preqr1g  3806  preqr1  3808  preq12b  3810  prel12  3811  elunii  3854  eluniab  3861  ssuni  3871  elinti  3893  elintab  3895  intss1  3899  intmin  3904  intab  3913  iineq2  3943  dfiin2g  3959  breq  4045  axsep2  4162  zfauscl  4163  inuni  4198  exmidexmid  4239  ss1o0el1  4240  exmid01  4241  exmidundif  4249  exmidundifim  4250  rext  4258  intid  4267  mss  4269  opth1  4279  opeqex  4293  frforeq3  4393  frirrg  4396  limeq  4423  nsuceq0g  4464  suctr  4467  snnex  4494  uniuni  4497  iunpw  4526  ordtriexmidlem  4566  ordtriexmidlem2  4567  ordtriexmid  4568  ontriexmidim  4569  ordtri2orexmid  4570  ontr2exmid  4572  ordtri2or2exmidlem  4573  onsucelsucexmidlem  4576  onsucelsucexmid  4577  ordsucunielexmid  4578  regexmidlem1  4580  reg2exmidlema  4581  regexmid  4582  reg2exmid  4583  elirr  4588  en2lp  4601  suc11g  4604  dtruex  4606  ordsoexmid  4609  nlimsucg  4613  onintexmid  4620  reg3exmidlemwe  4626  reg3exmid  4627  peano5  4645  limom  4661  0elnn  4666  nn0eln0  4667  nnregexmid  4668  xpeq1  4688  xpeq2  4689  opthprc  4725  xp11m  5120  funopg  5304  dffo4  5727  funopdmsn  5763  elunirn  5834  f1oiso  5894  canth  5896  eusvobj2  5929  acexmidlema  5934  acexmidlemb  5935  acexmidlemab  5937  acexmidlem2  5940  mpoeq123  6003  oprssdmm  6256  unielxp  6259  cnvf1o  6310  smoel  6385  tfr0dm  6407  frecabcl  6484  nnsucelsuc  6576  nntri3or  6578  nntri2  6579  nntri3  6582  nndceq  6584  nnmordi  6601  nnaordex  6613  elqsn0m  6689  qsel  6698  mapsn  6776  pw2f1odclem  6930  findcard2s  6986  undifdcss  7019  ctssdclemr  7213  nnnninf2  7228  exmidonfinlem  7300  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  finacn  7315  exmidaclem  7319  exmidontriimlem3  7334  exmidontriimlem4  7335  exmidontriim  7336  pw1ne3  7341  sucpw1ne3  7343  sucpw1nel3  7344  onntri35  7348  acnccim  7383  elni2  7426  addnidpig  7448  elinp  7586  suplocexprlemdisj  7832  suplocexprlemub  7835  pitonn  7960  peano1nnnn  7964  peano2nnnn  7965  peano5nnnn  8004  sup3exmid  9029  peano5nni  9038  1nn  9046  peano2nn  9047  dfuzi  9482  uz11  9670  elfzonlteqm1  10337  frec2uzltd  10546  0tonninf  10583  1tonninf  10584  wrdsymb0  11024  lsw0  11039  sumeq1  11608  prodeq1f  11805  nninfctlemfo  12303  ctiunct  12753  ssomct  12758  issubm  13246  isnsg  13480  releqgg  13498  eqgex  13499  resghm  13538  ghmeql  13545  issubrg  13925  lmodfopnelem2  14029  islssm  14061  islssmg  14062  lspsneq0  14130  istopg  14413  fiinbas  14463  topbas  14481  epttop  14504  restbasg  14582  icnpimaex  14625  lmcvg  14631  iscnp4  14632  cncnpi  14642  cnconst2  14647  cnptoprest  14653  cnptoprest2  14654  cnpdis  14656  lmss  14660  lmff  14663  txbas  14672  eltx  14673  txcnp  14685  txlm  14693  blssps  14841  blss  14842  blssexps  14843  blssex  14844  neibl  14905  metss  14908  metrest  14920  xmettx  14924  metcnp3  14925  tgioo  14968  tgqioo  14969  bdsep2  15755  bdzfauscl  15759  bj-indeq  15798  bj-nn0suc0  15819  bj-nnelirr  15822  bj-peano4  15824  bj-inf2vnlem2  15840  bj-nn0sucALT  15847  bj-findis  15848  strcollnft  15853  sscoll2  15857  2omap  15865  nninfsellemdc  15880  nninfsellemqall  15885  nnnninfex  15892