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  5833  elunirn  5906  f1oiso  5966  canth  5968  eusvobj2  6003  acexmidlema  6008  acexmidlemb  6009  acexmidlemab  6011  acexmidlem2  6014  mpoeq123  6079  oprssdmm  6333  unielxp  6336  cnvf1o  6389  smoel  6465  tfr0dm  6487  frecabcl  6564  nnsucelsuc  6658  nntri3or  6660  nntri2  6661  nntri3  6664  nndceq  6666  nnmordi  6683  nnaordex  6695  elqsn0m  6771  qsel  6780  mapsn  6858  en2m  6998  pw2f1odclem  7019  findcard2s  7078  elssdc  7093  eqsndc  7094  undifdcss  7114  ctssdclemr  7310  nnnninf2  7325  exmidonfinlem  7403  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  finacn  7418  exmidaclem  7422  exmidontriimlem3  7437  exmidontriimlem4  7438  exmidontriim  7439  iftrueb01  7440  pw1ne3  7447  sucpw1ne3  7449  sucpw1nel3  7450  onntri35  7454  acnccim  7490  elni2  7533  addnidpig  7555  elinp  7693  suplocexprlemdisj  7939  suplocexprlemub  7942  pitonn  8067  peano1nnnn  8071  peano2nnnn  8072  peano5nnnn  8111  sup3exmid  9136  peano5nni  9145  1nn  9153  peano2nn  9154  dfuzi  9589  uz11  9778  elfzonlteqm1  10454  frec2uzltd  10664  0tonninf  10701  1tonninf  10702  wrdsymb0  11145  lsw0  11160  swrdwrdsymbg  11244  sumeq1  11915  prodeq1f  12112  nninfctlemfo  12610  ctiunct  13060  ssomct  13065  issubm  13554  isnsg  13788  releqgg  13806  eqgex  13807  resghm  13846  ghmeql  13853  issubrg  14234  lmodfopnelem2  14338  islssm  14370  islssmg  14371  lspsneq0  14439  istopg  14722  fiinbas  14772  topbas  14790  epttop  14813  restbasg  14891  icnpimaex  14934  lmcvg  14940  iscnp4  14941  cncnpi  14951  cnconst2  14956  cnptoprest  14962  cnptoprest2  14963  cnpdis  14965  lmss  14969  lmff  14972  txbas  14981  eltx  14982  txcnp  14994  txlm  15002  blssps  15150  blss  15151  blssexps  15152  blssex  15153  neibl  15214  metss  15217  metrest  15229  xmettx  15233  metcnp3  15234  tgioo  15277  tgqioo  15278  uhgrm  15928  lpvtx  15929  incistruhgr  15940  umgrnloopv  15964  uhgredgm  15986  uhgrvtxedgiedgb  15993  upgredg2vtx  15998  uhgr2edg  16056  umgrvad2edg  16061  usgredg4  16065  uspgredg2vlem  16070  ushgredgedg  16076  subgruhgredgdm  16120  vtxd0nedgbfi  16149  1loopgrvd2fi  16155  wlk1walkdom  16209  bdsep2  16481  bdzfauscl  16485  bj-indeq  16524  bj-nn0suc0  16545  bj-nnelirr  16548  bj-peano4  16550  bj-inf2vnlem2  16566  bj-nn0sucALT  16573  bj-findis  16574  strcollnft  16579  sscoll2  16583  2omap  16594  nninfsellemdc  16612  nninfsellemqall  16617  nnnninfex  16624