Theorem eleq2 2293

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1393   = wceq 1395  ∃wex 1538   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12  2294  eleq2i  2296  eleq2d  2299  nelneq2  2331  clelsb2  2335  dvelimdc  2393  nelne1  2490  neleq2  2500  raleqf  2724  rexeqf  2725  reueq1f  2726  rmoeq1f  2727  rabeqf  2790  clel3g  2938  clel4  2940  sbcbi2  3080  sbcel2gv  3093  csbeq2  3149  sbnfc2  3186  difeq2  3317  uneq1  3352  ineq1  3399  nel02  3497  n0i  3498  disjel  3547  exsnrex  3709  sneqr  3841  preqr1g  3847  preqr1  3849  preq12b  3851  prel12  3852  elunii  3896  eluniab  3903  ssuni  3913  elinti  3935  elintab  3937  intss1  3941  intmin  3946  intab  3955  iineq2  3985  dfiin2g  4001  breq  4088  axsep2  4206  zfauscl  4207  inuni  4243  exmidexmid  4284  ss1o0el1  4285  exmid01  4286  exmidundif  4294  exmidundifim  4295  rext  4305  intid  4314  mss  4316  opth1  4326  opeqex  4340  frforeq3  4442  frirrg  4445  limeq  4472  nsuceq0g  4513  suctr  4516  snnex  4543  uniuni  4546  iunpw  4575  ordtriexmidlem  4615  ordtriexmidlem2  4616  ordtriexmid  4617  ontriexmidim  4618  ordtri2orexmid  4619  ontr2exmid  4621  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  onsucelsucexmid  4626  ordsucunielexmid  4627  regexmidlem1  4629  reg2exmidlema  4630  regexmid  4631  reg2exmid  4632  elirr  4637  en2lp  4650  suc11g  4653  dtruex  4655  ordsoexmid  4658  nlimsucg  4662  onintexmid  4669  reg3exmidlemwe  4675  reg3exmid  4676  peano5  4694  limom  4710  0elnn  4715  nn0eln0  4716  nnregexmid  4717  xpeq1  4737  xpeq2  4738  opthprc  4775  xp11m  5173  funopg  5358  dffo4  5791  funopdmsn  5829  elunirn  5902  f1oiso  5962  canth  5964  eusvobj2  5999  acexmidlema  6004  acexmidlemb  6005  acexmidlemab  6007  acexmidlem2  6010  mpoeq123  6075  oprssdmm  6329  unielxp  6332  cnvf1o  6385  smoel  6461  tfr0dm  6483  frecabcl  6560  nnsucelsuc  6654  nntri3or  6656  nntri2  6657  nntri3  6660  nndceq  6662  nnmordi  6679  nnaordex  6691  elqsn0m  6767  qsel  6776  mapsn  6854  en2m  6994  pw2f1odclem  7015  findcard2s  7072  elssdc  7087  eqsndc  7088  undifdcss  7108  ctssdclemr  7302  nnnninf2  7317  exmidonfinlem  7394  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  finacn  7409  exmidaclem  7413  exmidontriimlem3  7428  exmidontriimlem4  7429  exmidontriim  7430  iftrueb01  7431  pw1ne3  7438  sucpw1ne3  7440  sucpw1nel3  7441  onntri35  7445  acnccim  7481  elni2  7524  addnidpig  7546  elinp  7684  suplocexprlemdisj  7930  suplocexprlemub  7933  pitonn  8058  peano1nnnn  8062  peano2nnnn  8063  peano5nnnn  8102  sup3exmid  9127  peano5nni  9136  1nn  9144  peano2nn  9145  dfuzi  9580  uz11  9769  elfzonlteqm1  10445  frec2uzltd  10655  0tonninf  10692  1tonninf  10693  wrdsymb0  11136  lsw0  11151  swrdwrdsymbg  11235  sumeq1  11906  prodeq1f  12103  nninfctlemfo  12601  ctiunct  13051  ssomct  13056  issubm  13545  isnsg  13779  releqgg  13797  eqgex  13798  resghm  13837  ghmeql  13844  issubrg  14225  lmodfopnelem2  14329  islssm  14361  islssmg  14362  lspsneq0  14430  istopg  14713  fiinbas  14763  topbas  14781  epttop  14804  restbasg  14882  icnpimaex  14925  lmcvg  14931  iscnp4  14932  cncnpi  14942  cnconst2  14947  cnptoprest  14953  cnptoprest2  14954  cnpdis  14956  lmss  14960  lmff  14963  txbas  14972  eltx  14973  txcnp  14985  txlm  14993  blssps  15141  blss  15142  blssexps  15143  blssex  15144  neibl  15205  metss  15208  metrest  15220  xmettx  15224  metcnp3  15225  tgioo  15268  tgqioo  15269  uhgrm  15919  lpvtx  15920  incistruhgr  15931  umgrnloopv  15955  uhgredgm  15975  uhgrvtxedgiedgb  15982  upgredg2vtx  15987  uhgr2edg  16045  umgrvad2edg  16050  usgredg4  16054  uspgredg2vlem  16059  ushgredgedg  16065  vtxd0nedgbfi  16105  1loopgrvd2fi  16111  wlk1walkdom  16156  bdsep2  16417  bdzfauscl  16421  bj-indeq  16460  bj-nn0suc0  16481  bj-nnelirr  16484  bj-peano4  16486  bj-inf2vnlem2  16502  bj-nn0sucALT  16509  bj-findis  16510  strcollnft  16515  sscoll2  16519  2omap  16530  nninfsellemdc  16548  nninfsellemqall  16553  nnnninfex  16560