Theorem eleq2 2302

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12  2303  eleq2i  2305  eleq2d  2308  nelneq2  2340  clelsb2  2344  dvelimdc  2413  nelne1  2510  neleq2  2520  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2811  clel3g  2960  clel4  2962  sbcbi2  3102  sbcel2gv  3115  csbeq2  3171  sbnfc2  3208  difeq2  3341  uneq1  3376  ineq1  3425  nel02  3526  n0i  3527  disjel  3579  exsnrex  3751  sneqr  3885  preqr1g  3891  preqr1  3893  preq12b  3895  prel12  3896  elunii  3940  eluniab  3947  ssuni  3957  elinti  3979  elintab  3981  intss1  3985  intmin  3990  intab  3999  iineq2  4029  dfiin2g  4045  breq  4132  axsepg  4250  sepg  4251  zfausclOLD  4253  inuni  4291  exmidexmid  4333  ss1o0el1  4334  exmid01  4335  exmidundif  4343  exmidundifim  4344  rext  4355  intid  4364  mss  4366  opth1  4376  opeqex  4390  frforeq3  4492  frirrg  4495  limeq  4522  nsuceq0g  4563  suctr  4566  snnex  4594  uniuni  4597  iunpw  4626  ordtriexmidlem  4666  ordtriexmidlem2  4667  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  ontr2exmid  4672  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  onsucelsucexmid  4677  ordsucunielexmid  4678  regexmidlem1  4680  reg2exmidlema  4681  regexmid  4682  reg2exmid  4683  elirr  4688  en2lp  4701  suc11g  4704  dtruex  4706  ordsoexmid  4709  nlimsucg  4713  onintexmid  4720  reg3exmidlemwe  4726  reg3exmid  4727  peano5  4745  limom  4761  0elnn  4766  nn0eln0  4767  nnregexmid  4768  xpeq1  4788  xpeq2  4789  opthprc  4826  xp11m  5226  funopg  5411  dffo4  5856  funopdmsn  5895  elunirn  5972  f1oiso  6032  canth  6036  eusvobj2  6071  acexmidlema  6076  acexmidlemb  6077  acexmidlemab  6079  acexmidlem2  6082  mpoeq123  6147  oprssdmm  6405  unielxp  6408  cnvf1o  6461  smoel  6571  tfr0dm  6593  frecabcl  6670  nnsucelsuc  6764  nntri3or  6766  nntri2  6767  nntri3  6770  nndceq  6772  nnmordi  6789  nnaordex  6801  elqsn0m  6877  qsel  6886  mapsnd  6970  mapsn  6972  en2m  7113  pw2f1odclem  7134  findcard2s  7194  elssdc  7209  eqsndc  7210  undifdcss  7230  fissfi  7263  2omap  7318  ctssdclemr  7452  nnnninf2  7467  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  finacn  7560  exmidaclem  7564  exmidontriimlem3  7579  exmidontriimlem4  7580  exmidontriim  7581  iftrueb01  7582  pw1ne3  7589  sucpw1ne3  7591  sucpw1nel3  7592  onntri35  7596  acnccim  7638  elni2  7681  addnidpig  7703  elinp  7841  suplocexprlemdisj  8087  suplocexprlemub  8090  pitonn  8215  peano1nnnn  8219  peano2nnnn  8220  peano5nnnn  8259  sup3exmid  9289  indval  9298  peano5nni  9309  1nn  9317  peano2nn  9318  dfuzi  9760  uz11  9954  elfzonlteqm1  10638  frec2uzltd  10853  0tonninf  10890  1tonninf  10891  hashfibclem  11296  hashf1lem2  11300  wrdsymb0  11351  lsw0  11366  swrdwrdsymbg  11450  sumeq1  12137  prodeq1f  12335  nninfctlemfo  12833  ballotfilemcdc  13272  ballotfilem7  13328  ctiunct  13380  ssomct  13385  issubm  13828  isnsg  14054  releqgg  14072  eqgex  14073  resghm  14112  ghmeql  14119  issubrg  14578  lmodfopnelem2  14711  islssm  14743  islssmg  14744  lspsneq0  14812  istopg  15149  fiinbas  15199  topbas  15217  epttop  15240  restbasg  15318  icnpimaex  15361  lmcvg  15367  iscnp4  15368  cncnpi  15378  cnconst2  15383  cnptoprest  15389  cnptoprest2  15390  cnpdis  15392  lmss  15396  lmff  15399  txbas  15408  eltx  15409  txcnp  15421  txlm  15429  blssps  15577  blss  15578  blssexps  15579  blssex  15580  neibl  15641  metss  15644  metrest  15656  xmettx  15660  metcnp3  15661  tgioo  15704  tgqioo  15705  uhgrm  16417  lpvtx  16418  incistruhgr  16429  umgrnloopv  16453  uhgredgm  16475  uhgrvtxedgiedgb  16482  upgredg2vtx  16487  uhgr2edg  16545  umgrvad2edg  16550  usgredg4  16554  uspgredg2vlem  16559  ushgredgedg  16565  subgruhgredgdm  16609  vtxd0nedgbfi  16638  1loopgrvd2fi  16644  wlk1walkdom  16698  bdsep2  17010  bdsepg  17014  bj-indeq  17053  bj-nn0suc0  17074  bj-nnelirr  17077  bj-peano4  17079  bj-inf2vnlem2  17095  bj-nn0sucALT  17102  bj-findis  17103  strcollnft  17108  sscoll2  17112  nninfsellemdc  17151  nninfsellemqall  17156  nnnninfex  17163