Theorem eleq2 2296

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

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

This theorem is referenced by:  eleq12  2297  eleq2i  2299  eleq2d  2302  nelneq2  2334  clelsb2  2338  dvelimdc  2405  nelne1  2502  neleq2  2512  raleqf  2737  rexeqf  2738  reueq1f  2739  rmoeq1f  2740  rabeqf  2803  clel3g  2951  clel4  2953  sbcbi2  3093  sbcel2gv  3106  csbeq2  3162  sbnfc2  3199  difeq2  3331  uneq1  3366  ineq1  3415  nel02  3513  n0i  3514  disjel  3563  exsnrex  3731  sneqr  3864  preqr1g  3870  preqr1  3872  preq12b  3874  prel12  3875  elunii  3919  eluniab  3926  ssuni  3936  elinti  3958  elintab  3960  intss1  3964  intmin  3969  intab  3978  iineq2  4008  dfiin2g  4024  breq  4111  axsep2  4229  zfauscl  4230  inuni  4267  exmidexmid  4309  ss1o0el1  4310  exmid01  4311  exmidundif  4319  exmidundifim  4320  rext  4331  intid  4340  mss  4342  opth1  4352  opeqex  4366  frforeq3  4468  frirrg  4471  limeq  4498  nsuceq0g  4539  suctr  4542  snnex  4569  uniuni  4572  iunpw  4601  ordtriexmidlem  4641  ordtriexmidlem2  4642  ordtriexmid  4643  ontriexmidim  4644  ordtri2orexmid  4645  ontr2exmid  4647  ordtri2or2exmidlem  4648  onsucelsucexmidlem  4651  onsucelsucexmid  4652  ordsucunielexmid  4653  regexmidlem1  4655  reg2exmidlema  4656  regexmid  4657  reg2exmid  4658  elirr  4663  en2lp  4676  suc11g  4679  dtruex  4681  ordsoexmid  4684  nlimsucg  4688  onintexmid  4695  reg3exmidlemwe  4701  reg3exmid  4702  peano5  4720  limom  4736  0elnn  4741  nn0eln0  4742  nnregexmid  4743  xpeq1  4763  xpeq2  4764  opthprc  4801  xp11m  5201  funopg  5386  dffo4  5825  funopdmsn  5864  elunirn  5939  f1oiso  5999  canth  6001  eusvobj2  6036  acexmidlema  6041  acexmidlemb  6042  acexmidlemab  6044  acexmidlem2  6047  mpoeq123  6112  oprssdmm  6365  unielxp  6368  cnvf1o  6421  smoel  6531  tfr0dm  6553  frecabcl  6630  nnsucelsuc  6724  nntri3or  6726  nntri2  6727  nntri3  6730  nndceq  6732  nnmordi  6749  nnaordex  6761  elqsn0m  6837  qsel  6846  mapsnd  6923  mapsn  6925  en2m  7066  pw2f1odclem  7087  findcard2s  7147  elssdc  7162  eqsndc  7163  undifdcss  7183  fissfi  7216  2omap  7269  ctssdclemr  7403  nnnninf2  7418  exmidonfinlem  7496  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  finacn  7511  exmidaclem  7515  exmidontriimlem3  7530  exmidontriimlem4  7531  exmidontriim  7532  iftrueb01  7533  pw1ne3  7540  sucpw1ne3  7542  sucpw1nel3  7543  onntri35  7547  acnccim  7586  elni2  7629  addnidpig  7651  elinp  7789  suplocexprlemdisj  8035  suplocexprlemub  8038  pitonn  8163  peano1nnnn  8167  peano2nnnn  8168  peano5nnnn  8207  sup3exmid  9231  peano5nni  9240  1nn  9248  peano2nn  9249  dfuzi  9688  uz11  9877  elfzonlteqm1  10555  frec2uzltd  10765  0tonninf  10802  1tonninf  10803  hashfibclem  11206  wrdsymb0  11257  lsw0  11272  swrdwrdsymbg  11356  sumeq1  12040  prodeq1f  12238  nninfctlemfo  12736  ctiunct  13191  ssomct  13196  issubm  13685  isnsg  13919  releqgg  13937  eqgex  13938  resghm  13977  ghmeql  13984  issubrg  14366  lmodfopnelem2  14473  islssm  14505  islssmg  14506  lspsneq0  14574  istopg  14864  fiinbas  14914  topbas  14932  epttop  14955  restbasg  15033  icnpimaex  15076  lmcvg  15082  iscnp4  15083  cncnpi  15093  cnconst2  15098  cnptoprest  15104  cnptoprest2  15105  cnpdis  15107  lmss  15111  lmff  15114  txbas  15123  eltx  15124  txcnp  15136  txlm  15144  blssps  15292  blss  15293  blssexps  15294  blssex  15295  neibl  15356  metss  15359  metrest  15371  xmettx  15375  metcnp3  15376  tgioo  15419  tgqioo  15420  uhgrm  16073  lpvtx  16074  incistruhgr  16085  umgrnloopv  16109  uhgredgm  16131  uhgrvtxedgiedgb  16138  upgredg2vtx  16143  uhgr2edg  16201  umgrvad2edg  16206  usgredg4  16210  uspgredg2vlem  16215  ushgredgedg  16221  subgruhgredgdm  16265  vtxd0nedgbfi  16294  1loopgrvd2fi  16300  wlk1walkdom  16354  bdsep2  16656  bdzfauscl  16660  bj-indeq  16699  bj-nn0suc0  16720  bj-nnelirr  16723  bj-peano4  16725  bj-inf2vnlem2  16741  bj-nn0sucALT  16748  bj-findis  16749  strcollnft  16754  sscoll2  16758  nninfsellemdc  16788  nninfsellemqall  16793  nnnninfex  16800