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  11637  prodeq1f  11834  nninfctlemfo  12332  ctiunct  12782  ssomct  12787  issubm  13275  isnsg  13509  releqgg  13527  eqgex  13528  resghm  13567  ghmeql  13574  issubrg  13954  lmodfopnelem2  14058  islssm  14090  islssmg  14091  lspsneq0  14159  istopg  14442  fiinbas  14492  topbas  14510  epttop  14533  restbasg  14611  icnpimaex  14654  lmcvg  14660  iscnp4  14661  cncnpi  14671  cnconst2  14676  cnptoprest  14682  cnptoprest2  14683  cnpdis  14685  lmss  14689  lmff  14692  txbas  14701  eltx  14702  txcnp  14714  txlm  14722  blssps  14870  blss  14871  blssexps  14872  blssex  14873  neibl  14934  metss  14937  metrest  14949  xmettx  14953  metcnp3  14954  tgioo  14997  tgqioo  14998  bdsep2  15784  bdzfauscl  15788  bj-indeq  15827  bj-nn0suc0  15848  bj-nnelirr  15851  bj-peano4  15853  bj-inf2vnlem2  15869  bj-nn0sucALT  15876  bj-findis  15877  strcollnft  15882  sscoll2  15886  2omap  15894  nninfsellemdc  15909  nninfsellemqall  15914  nnnninfex  15921