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  9287  indval  9296  peano5nni  9307  1nn  9315  peano2nn  9316  dfuzi  9756  uz11  9945  elfzonlteqm1  10628  frec2uzltd  10840  0tonninf  10877  1tonninf  10878  hashfibclem  11282  hashf1lem2  11286  wrdsymb0  11337  lsw0  11352  swrdwrdsymbg  11436  sumeq1  12121  prodeq1f  12319  nninfctlemfo  12817  ballotfilemcdc  13223  ballotfilem7  13279  ctiunct  13331  ssomct  13336  issubm  13779  isnsg  14005  releqgg  14023  eqgex  14024  resghm  14063  ghmeql  14070  issubrg  14529  lmodfopnelem2  14662  islssm  14694  islssmg  14695  lspsneq0  14763  istopg  15100  fiinbas  15150  topbas  15168  epttop  15191  restbasg  15269  icnpimaex  15312  lmcvg  15318  iscnp4  15319  cncnpi  15329  cnconst2  15334  cnptoprest  15340  cnptoprest2  15341  cnpdis  15343  lmss  15347  lmff  15350  txbas  15359  eltx  15360  txcnp  15372  txlm  15380  blssps  15528  blss  15529  blssexps  15530  blssex  15531  neibl  15592  metss  15595  metrest  15607  xmettx  15611  metcnp3  15612  tgioo  15655  tgqioo  15656  uhgrm  16319  lpvtx  16320  incistruhgr  16331  umgrnloopv  16355  uhgredgm  16377  uhgrvtxedgiedgb  16384  upgredg2vtx  16389  uhgr2edg  16447  umgrvad2edg  16452  usgredg4  16456  uspgredg2vlem  16461  ushgredgedg  16467  subgruhgredgdm  16511  vtxd0nedgbfi  16540  1loopgrvd2fi  16546  wlk1walkdom  16600  bdsep2  16912  bdsepg  16916  bj-indeq  16955  bj-nn0suc0  16976  bj-nnelirr  16979  bj-peano4  16981  bj-inf2vnlem2  16997  bj-nn0sucALT  17004  bj-findis  17005  strcollnft  17010  sscoll2  17014  nninfsellemdc  17053  nninfsellemqall  17058  nnnninfex  17065