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 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced 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  3578  exsnrex  3747  sneqr  3880  preqr1g  3886  preqr1  3888  preq12b  3890  prel12  3891  elunii  3935  eluniab  3942  ssuni  3952  elinti  3974  elintab  3976  intss1  3980  intmin  3985  intab  3994  iineq2  4024  dfiin2g  4040  breq  4127  axsepg  4245  sepg  4246  zfausclOLD  4248  inuni  4286  exmidexmid  4328  ss1o0el1  4329  exmid01  4330  exmidundif  4338  exmidundifim  4339  rext  4350  intid  4359  mss  4361  opth1  4371  opeqex  4385  frforeq3  4487  frirrg  4490  limeq  4517  nsuceq0g  4558  suctr  4561  snnex  4589  uniuni  4592  iunpw  4621  ordtriexmidlem  4661  ordtriexmidlem2  4662  ordtriexmid  4663  ontriexmidim  4664  ordtri2orexmid  4665  ontr2exmid  4667  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  onsucelsucexmid  4672  ordsucunielexmid  4673  regexmidlem1  4675  reg2exmidlema  4676  regexmid  4677  reg2exmid  4678  elirr  4683  en2lp  4696  suc11g  4699  dtruex  4701  ordsoexmid  4704  nlimsucg  4708  onintexmid  4715  reg3exmidlemwe  4721  reg3exmid  4722  peano5  4740  limom  4756  0elnn  4761  nn0eln0  4762  nnregexmid  4763  xpeq1  4783  xpeq2  4784  opthprc  4821  xp11m  5221  funopg  5406  dffo4  5847  funopdmsn  5886  elunirn  5962  f1oiso  6022  canth  6026  eusvobj2  6061  acexmidlema  6066  acexmidlemb  6067  acexmidlemab  6069  acexmidlem2  6072  mpoeq123  6137  oprssdmm  6395  unielxp  6398  cnvf1o  6451  smoel  6561  tfr0dm  6583  frecabcl  6660  nnsucelsuc  6754  nntri3or  6756  nntri2  6757  nntri3  6760  nndceq  6762  nnmordi  6779  nnaordex  6791  elqsn0m  6867  qsel  6876  mapsnd  6960  mapsn  6962  en2m  7103  pw2f1odclem  7124  findcard2s  7184  elssdc  7199  eqsndc  7200  undifdcss  7220  fissfi  7253  2omap  7308  ctssdclemr  7442  nnnninf2  7457  exmidonfinlem  7535  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  finacn  7550  exmidaclem  7554  exmidontriimlem3  7569  exmidontriimlem4  7570  exmidontriim  7571  iftrueb01  7572  pw1ne3  7579  sucpw1ne3  7581  sucpw1nel3  7582  onntri35  7586  acnccim  7628  elni2  7671  addnidpig  7693  elinp  7831  suplocexprlemdisj  8077  suplocexprlemub  8080  pitonn  8205  peano1nnnn  8209  peano2nnnn  8210  peano5nnnn  8249  sup3exmid  9277  peano5nni  9286  1nn  9294  peano2nn  9295  dfuzi  9735  uz11  9924  elfzonlteqm1  10606  frec2uzltd  10818  0tonninf  10855  1tonninf  10856  hashfibclem  11260  hashf1lem2  11264  wrdsymb0  11315  lsw0  11330  swrdwrdsymbg  11414  sumeq1  12099  prodeq1f  12297  nninfctlemfo  12795  ballotfilemcdc  13201  ballotfilem7  13257  ctiunct  13309  ssomct  13314  issubm  13756  isnsg  13982  releqgg  14000  eqgex  14001  resghm  14040  ghmeql  14047  issubrg  14502  lmodfopnelem2  14634  islssm  14666  islssmg  14667  lspsneq0  14735  istopg  15023  fiinbas  15073  topbas  15091  epttop  15114  restbasg  15192  icnpimaex  15235  lmcvg  15241  iscnp4  15242  cncnpi  15252  cnconst2  15257  cnptoprest  15263  cnptoprest2  15264  cnpdis  15266  lmss  15270  lmff  15273  txbas  15282  eltx  15283  txcnp  15295  txlm  15303  blssps  15451  blss  15452  blssexps  15453  blssex  15454  neibl  15515  metss  15518  metrest  15530  xmettx  15534  metcnp3  15535  tgioo  15578  tgqioo  15579  uhgrm  16233  lpvtx  16234  incistruhgr  16245  umgrnloopv  16269  uhgredgm  16291  uhgrvtxedgiedgb  16298  upgredg2vtx  16303  uhgr2edg  16361  umgrvad2edg  16366  usgredg4  16370  uspgredg2vlem  16375  ushgredgedg  16381  subgruhgredgdm  16425  vtxd0nedgbfi  16454  1loopgrvd2fi  16460  wlk1walkdom  16514  bdsep2  16826  bdsepg  16830  bj-indeq  16869  bj-nn0suc0  16890  bj-nnelirr  16893  bj-peano4  16895  bj-inf2vnlem2  16911  bj-nn0sucALT  16918  bj-findis  16919  strcollnft  16924  sscoll2  16928  nninfsellemdc  16958  nninfsellemqall  16963  nnnninfex  16970