Theorem eleq2 2295

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1395   = wceq 1397  ∃wex 1540   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  eleq12  2296  eleq2i  2298  eleq2d  2301  nelneq2  2333  clelsb2  2337  dvelimdc  2395  nelne1  2492  neleq2  2502  raleqf  2726  rexeqf  2727  reueq1f  2728  rmoeq1f  2729  rabeqf  2792  clel3g  2940  clel4  2942  sbcbi2  3082  sbcel2gv  3095  csbeq2  3151  sbnfc2  3188  difeq2  3319  uneq1  3354  ineq1  3401  nel02  3499  n0i  3500  disjel  3549  exsnrex  3711  sneqr  3843  preqr1g  3849  preqr1  3851  preq12b  3853  prel12  3854  elunii  3898  eluniab  3905  ssuni  3915  elinti  3937  elintab  3939  intss1  3943  intmin  3948  intab  3957  iineq2  3987  dfiin2g  4003  breq  4090  axsep2  4208  zfauscl  4209  inuni  4245  exmidexmid  4286  ss1o0el1  4287  exmid01  4288  exmidundif  4296  exmidundifim  4297  rext  4307  intid  4316  mss  4318  opth1  4328  opeqex  4342  frforeq3  4444  frirrg  4447  limeq  4474  nsuceq0g  4515  suctr  4518  snnex  4545  uniuni  4548  iunpw  4577  ordtriexmidlem  4617  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  onsucelsucexmid  4628  ordsucunielexmid  4629  regexmidlem1  4631  reg2exmidlema  4632  regexmid  4633  reg2exmid  4634  elirr  4639  en2lp  4652  suc11g  4655  dtruex  4657  ordsoexmid  4660  nlimsucg  4664  onintexmid  4671  reg3exmidlemwe  4677  reg3exmid  4678  peano5  4696  limom  4712  0elnn  4717  nn0eln0  4718  nnregexmid  4719  xpeq1  4739  xpeq2  4740  opthprc  4777  xp11m  5175  funopg  5360  dffo4  5795  funopdmsn  5834  elunirn  5907  f1oiso  5967  canth  5969  eusvobj2  6004  acexmidlema  6009  acexmidlemb  6010  acexmidlemab  6012  acexmidlem2  6015  mpoeq123  6080  oprssdmm  6334  unielxp  6337  cnvf1o  6390  smoel  6466  tfr0dm  6488  frecabcl  6565  nnsucelsuc  6659  nntri3or  6661  nntri2  6662  nntri3  6665  nndceq  6667  nnmordi  6684  nnaordex  6696  elqsn0m  6772  qsel  6781  mapsn  6859  en2m  6999  pw2f1odclem  7020  findcard2s  7079  elssdc  7094  eqsndc  7095  undifdcss  7115  ctssdclemr  7311  nnnninf2  7326  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  finacn  7419  exmidaclem  7423  exmidontriimlem3  7438  exmidontriimlem4  7439  exmidontriim  7440  iftrueb01  7441  pw1ne3  7448  sucpw1ne3  7450  sucpw1nel3  7451  onntri35  7455  acnccim  7491  elni2  7534  addnidpig  7556  elinp  7694  suplocexprlemdisj  7940  suplocexprlemub  7943  pitonn  8068  peano1nnnn  8072  peano2nnnn  8073  peano5nnnn  8112  sup3exmid  9137  peano5nni  9146  1nn  9154  peano2nn  9155  dfuzi  9590  uz11  9779  elfzonlteqm1  10456  frec2uzltd  10666  0tonninf  10703  1tonninf  10704  wrdsymb0  11150  lsw0  11165  swrdwrdsymbg  11249  sumeq1  11920  prodeq1f  12118  nninfctlemfo  12616  ctiunct  13066  ssomct  13071  issubm  13560  isnsg  13794  releqgg  13812  eqgex  13813  resghm  13852  ghmeql  13859  issubrg  14241  lmodfopnelem2  14345  islssm  14377  islssmg  14378  lspsneq0  14446  istopg  14729  fiinbas  14779  topbas  14797  epttop  14820  restbasg  14898  icnpimaex  14941  lmcvg  14947  iscnp4  14948  cncnpi  14958  cnconst2  14963  cnptoprest  14969  cnptoprest2  14970  cnpdis  14972  lmss  14976  lmff  14979  txbas  14988  eltx  14989  txcnp  15001  txlm  15009  blssps  15157  blss  15158  blssexps  15159  blssex  15160  neibl  15221  metss  15224  metrest  15236  xmettx  15240  metcnp3  15241  tgioo  15284  tgqioo  15285  uhgrm  15935  lpvtx  15936  incistruhgr  15947  umgrnloopv  15971  uhgredgm  15993  uhgrvtxedgiedgb  16000  upgredg2vtx  16005  uhgr2edg  16063  umgrvad2edg  16068  usgredg4  16072  uspgredg2vlem  16077  ushgredgedg  16083  subgruhgredgdm  16127  vtxd0nedgbfi  16156  1loopgrvd2fi  16162  wlk1walkdom  16216  bdsep2  16507  bdzfauscl  16511  bj-indeq  16550  bj-nn0suc0  16571  bj-nnelirr  16574  bj-peano4  16576  bj-inf2vnlem2  16592  bj-nn0sucALT  16599  bj-findis  16600  strcollnft  16605  sscoll2  16609  2omap  16620  nninfsellemdc  16638  nninfsellemqall  16643  nnnninfex  16650