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  9248  peano5nni  9257  1nn  9265  peano2nn  9266  dfuzi  9706  uz11  9895  elfzonlteqm1  10577  frec2uzltd  10789  0tonninf  10826  1tonninf  10827  hashfibclem  11231  wrdsymb0  11282  lsw0  11297  swrdwrdsymbg  11381  sumeq1  12065  prodeq1f  12263  nninfctlemfo  12761  ballotfilemcdc  13167  ballotfilem7  13223  ctiunct  13275  ssomct  13280  issubm  13727  isnsg  13955  releqgg  13973  eqgex  13974  resghm  14013  ghmeql  14020  issubrg  14467  lmodfopnelem2  14599  islssm  14631  islssmg  14632  lspsneq0  14700  istopg  14990  fiinbas  15040  topbas  15058  epttop  15081  restbasg  15159  icnpimaex  15202  lmcvg  15208  iscnp4  15209  cncnpi  15219  cnconst2  15224  cnptoprest  15230  cnptoprest2  15231  cnpdis  15233  lmss  15237  lmff  15240  txbas  15249  eltx  15250  txcnp  15262  txlm  15270  blssps  15418  blss  15419  blssexps  15420  blssex  15421  neibl  15482  metss  15485  metrest  15497  xmettx  15501  metcnp3  15502  tgioo  15545  tgqioo  15546  uhgrm  16199  lpvtx  16200  incistruhgr  16211  umgrnloopv  16235  uhgredgm  16257  uhgrvtxedgiedgb  16264  upgredg2vtx  16269  uhgr2edg  16327  umgrvad2edg  16332  usgredg4  16336  uspgredg2vlem  16341  ushgredgedg  16347  subgruhgredgdm  16391  vtxd0nedgbfi  16420  1loopgrvd2fi  16426  wlk1walkdom  16480  bdsep2  16782  bdzfauscl  16786  bj-indeq  16825  bj-nn0suc0  16846  bj-nnelirr  16849  bj-peano4  16851  bj-inf2vnlem2  16867  bj-nn0sucALT  16874  bj-findis  16875  strcollnft  16880  sscoll2  16884  nninfsellemdc  16914  nninfsellemqall  16919  nnnninfex  16926