Theorem eleq2 2298

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 2228	. . . . . 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 2230	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2230	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

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

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleq12  2299  eleq2i  2301  eleq2d  2304  nelneq2  2336  clelsb2  2340  dvelimdc  2407  nelne1  2504  neleq2  2514  raleqf  2739  rexeqf  2740  reueq1f  2741  rmoeq1f  2742  rabeqf  2805  clel3g  2954  clel4  2956  sbcbi2  3096  sbcel2gv  3109  csbeq2  3165  sbnfc2  3202  difeq2  3335  uneq1  3370  ineq1  3419  nel02  3517  n0i  3518  disjel  3567  exsnrex  3736  sneqr  3869  preqr1g  3875  preqr1  3877  preq12b  3879  prel12  3880  elunii  3924  eluniab  3931  ssuni  3941  elinti  3963  elintab  3965  intss1  3969  intmin  3974  intab  3983  iineq2  4013  dfiin2g  4029  breq  4116  axsep2  4234  zfauscl  4235  inuni  4272  exmidexmid  4314  ss1o0el1  4315  exmid01  4316  exmidundif  4324  exmidundifim  4325  rext  4336  intid  4345  mss  4347  opth1  4357  opeqex  4371  frforeq3  4473  frirrg  4476  limeq  4503  nsuceq0g  4544  suctr  4547  snnex  4574  uniuni  4577  iunpw  4606  ordtriexmidlem  4646  ordtriexmidlem2  4647  ordtriexmid  4648  ontriexmidim  4649  ordtri2orexmid  4650  ontr2exmid  4652  ordtri2or2exmidlem  4653  onsucelsucexmidlem  4656  onsucelsucexmid  4657  ordsucunielexmid  4658  regexmidlem1  4660  reg2exmidlema  4661  regexmid  4662  reg2exmid  4663  elirr  4668  en2lp  4681  suc11g  4684  dtruex  4686  ordsoexmid  4689  nlimsucg  4693  onintexmid  4700  reg3exmidlemwe  4706  reg3exmid  4707  peano5  4725  limom  4741  0elnn  4746  nn0eln0  4747  nnregexmid  4748  xpeq1  4768  xpeq2  4769  opthprc  4806  xp11m  5206  funopg  5391  dffo4  5830  funopdmsn  5869  elunirn  5945  f1oiso  6005  canth  6009  eusvobj2  6044  acexmidlema  6049  acexmidlemb  6050  acexmidlemab  6052  acexmidlem2  6055  mpoeq123  6120  oprssdmm  6378  unielxp  6381  cnvf1o  6434  smoel  6544  tfr0dm  6566  frecabcl  6643  nnsucelsuc  6737  nntri3or  6739  nntri2  6740  nntri3  6743  nndceq  6745  nnmordi  6762  nnaordex  6774  elqsn0m  6850  qsel  6859  mapsnd  6936  mapsn  6938  en2m  7079  pw2f1odclem  7100  findcard2s  7160  elssdc  7175  eqsndc  7176  undifdcss  7196  fissfi  7229  2omap  7282  ctssdclemr  7416  nnnninf2  7431  exmidonfinlem  7509  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  finacn  7524  exmidaclem  7528  exmidontriimlem3  7543  exmidontriimlem4  7544  exmidontriim  7545  iftrueb01  7546  pw1ne3  7553  sucpw1ne3  7555  sucpw1nel3  7556  onntri35  7560  acnccim  7602  elni2  7645  addnidpig  7667  elinp  7805  suplocexprlemdisj  8051  suplocexprlemub  8054  pitonn  8179  peano1nnnn  8183  peano2nnnn  8184  peano5nnnn  8223  sup3exmid  9251  peano5nni  9260  1nn  9268  peano2nn  9269  dfuzi  9709  uz11  9898  elfzonlteqm1  10580  frec2uzltd  10792  0tonninf  10829  1tonninf  10830  hashfibclem  11234  wrdsymb0  11285  lsw0  11300  swrdwrdsymbg  11384  sumeq1  12068  prodeq1f  12266  nninfctlemfo  12764  ballotfilemcdc  13170  ballotfilem7  13226  ctiunct  13278  ssomct  13283  issubm  13730  isnsg  13958  releqgg  13976  eqgex  13977  resghm  14016  ghmeql  14023  issubrg  14470  lmodfopnelem2  14602  islssm  14634  islssmg  14635  lspsneq0  14703  istopg  14993  fiinbas  15043  topbas  15061  epttop  15084  restbasg  15162  icnpimaex  15205  lmcvg  15211  iscnp4  15212  cncnpi  15222  cnconst2  15227  cnptoprest  15233  cnptoprest2  15234  cnpdis  15236  lmss  15240  lmff  15243  txbas  15252  eltx  15253  txcnp  15265  txlm  15273  blssps  15421  blss  15422  blssexps  15423  blssex  15424  neibl  15485  metss  15488  metrest  15500  xmettx  15504  metcnp3  15505  tgioo  15548  tgqioo  15549  uhgrm  16202  lpvtx  16203  incistruhgr  16214  umgrnloopv  16238  uhgredgm  16260  uhgrvtxedgiedgb  16267  upgredg2vtx  16272  uhgr2edg  16330  umgrvad2edg  16335  usgredg4  16339  uspgredg2vlem  16344  ushgredgedg  16350  subgruhgredgdm  16394  vtxd0nedgbfi  16423  1loopgrvd2fi  16429  wlk1walkdom  16483  bdsep2  16795  bdzfauscl  16799  bj-indeq  16838  bj-nn0suc0  16859  bj-nnelirr  16862  bj-peano4  16864  bj-inf2vnlem2  16880  bj-nn0sucALT  16887  bj-findis  16888  strcollnft  16893  sscoll2  16897  nninfsellemdc  16927  nninfsellemqall  16932  nnnninfex  16939