Theorem eleq2 2163

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 2094	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 119	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1505	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	anbi2d 455	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	exbidv 1764	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2096	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2096	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1297   = wceq 1299  ∃wex 1436   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096

This theorem is referenced by:  eleq12  2164  eleq2i  2166  eleq2d  2169  nelneq2  2201  clelsb4  2205  dvelimdc  2260  nelne1  2357  neleq2  2367  raleqf  2580  rexeqf  2581  reueq1f  2582  rmoeq1f  2583  rabeqf  2631  clel3g  2773  clel4  2775  sbcbi2  2911  sbcel2gv  2924  sbnfc2  3010  difeq2  3135  uneq1  3170  ineq1  3217  n0i  3315  disjel  3364  exsnrex  3513  sneqr  3634  preqr1g  3640  preqr1  3642  preq12b  3644  prel12  3645  elunii  3688  eluniab  3695  ssuni  3705  elinti  3727  elintab  3729  intss1  3733  intmin  3738  intab  3747  iineq2  3777  dfiin2g  3793  breq  3877  axsep2  3987  zfauscl  3988  inuni  4020  exmidexmid  4060  exmid01  4061  exmidundif  4067  exmidundifim  4068  rext  4075  intid  4084  mss  4086  opth1  4096  opeqex  4109  frforeq3  4207  frirrg  4210  limeq  4237  nsuceq0g  4278  suctr  4281  snnex  4307  uniuni  4310  iunpw  4339  ordtriexmidlem  4373  ordtriexmidlem2  4374  ordtriexmid  4375  ordtri2orexmid  4376  ontr2exmid  4378  ordtri2or2exmidlem  4379  onsucelsucexmidlem  4382  onsucelsucexmid  4383  ordsucunielexmid  4384  regexmidlem1  4386  reg2exmidlema  4387  regexmid  4388  reg2exmid  4389  elirr  4394  en2lp  4407  suc11g  4410  dtruex  4412  ordsoexmid  4415  nlimsucg  4419  onintexmid  4425  reg3exmidlemwe  4431  reg3exmid  4432  peano5  4450  limom  4465  0elnn  4470  nn0eln0  4471  nnregexmid  4472  xpeq1  4491  xpeq2  4492  opthprc  4528  xp11m  4913  funopg  5093  dffo4  5500  elunirn  5599  f1oiso  5659  eusvobj2  5692  acexmidlema  5697  acexmidlemb  5698  acexmidlemab  5700  acexmidlem2  5703  mpoeq123  5762  unielxp  6002  cnvf1o  6052  smoel  6127  tfr0dm  6149  frecabcl  6226  nnsucelsuc  6317  nntri3or  6319  nntri2  6320  nntri3  6323  nndceq  6325  nnmordi  6342  nnaordex  6353  elqsn0m  6427  qsel  6436  mapsn  6514  findcard2s  6713  undifdcss  6740  ctssdclemr  6911  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  elni2  7023  addnidpig  7045  elinp  7183  pitonn  7535  peano1nnnn  7539  peano2nnnn  7540  peano5nnnn  7577  sup3exmid  8573  peano5nni  8581  1nn  8589  peano2nn  8590  dfuzi  9013  uz11  9198  elfzonlteqm1  9828  frec2uzltd  10017  0tonninf  10053  1tonninf  10054  sumeq1  10963  istopg  11948  fiinbas  11998  topbas  12018  epttop  12041  restbasg  12119  icnpimaex  12161  lmcvg  12167  iscnp4  12168  cncnpi  12178  cnconst2  12183  cnptoprest  12189  cnptoprest2  12190  cnpdis  12192  lmss  12196  lmff  12199  txbas  12208  eltx  12209  txcnp  12221  txlm  12229  blssps  12355  blss  12356  blssexps  12357  blssex  12358  neibl  12419  metss  12422  metrest  12434  metcnp3  12435  tgioo  12465  tgqioo  12466  bdsep2  12665  bdzfauscl  12669  bj-indeq  12712  bj-nn0suc0  12733  bj-nnelirr  12736  bj-peano4  12738  bj-inf2vnlem2  12754  bj-nn0sucALT  12761  bj-findis  12762  nninfsellemdc  12790  nninfsellemqall  12795