Theorem eleq2 2230

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1341   = wceq 1343  ∃wex 1480   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleq12  2231  eleq2i  2233  eleq2d  2236  nelneq2  2268  clelsb2  2272  dvelimdc  2329  nelne1  2426  neleq2  2436  raleqf  2657  rexeqf  2658  reueq1f  2659  rmoeq1f  2660  rabeqf  2716  clel3g  2860  clel4  2862  sbcbi2  3001  sbcel2gv  3014  csbeq2  3069  sbnfc2  3105  difeq2  3234  uneq1  3269  ineq1  3316  n0i  3414  disjel  3463  exsnrex  3618  sneqr  3740  preqr1g  3746  preqr1  3748  preq12b  3750  prel12  3751  elunii  3794  eluniab  3801  ssuni  3811  elinti  3833  elintab  3835  intss1  3839  intmin  3844  intab  3853  iineq2  3883  dfiin2g  3899  breq  3984  axsep2  4101  zfauscl  4102  inuni  4134  exmidexmid  4175  ss1o0el1  4176  exmid01  4177  exmidundif  4185  exmidundifim  4186  rext  4193  intid  4202  mss  4204  opth1  4214  opeqex  4227  frforeq3  4325  frirrg  4328  limeq  4355  nsuceq0g  4396  suctr  4399  snnex  4426  uniuni  4429  iunpw  4458  ordtriexmidlem  4496  ordtriexmidlem2  4497  ordtriexmid  4498  ontriexmidim  4499  ordtri2orexmid  4500  ontr2exmid  4502  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  onsucelsucexmid  4507  ordsucunielexmid  4508  regexmidlem1  4510  reg2exmidlema  4511  regexmid  4512  reg2exmid  4513  elirr  4518  en2lp  4531  suc11g  4534  dtruex  4536  ordsoexmid  4539  nlimsucg  4543  onintexmid  4550  reg3exmidlemwe  4556  reg3exmid  4557  peano5  4575  limom  4591  0elnn  4596  nn0eln0  4597  nnregexmid  4598  xpeq1  4618  xpeq2  4619  opthprc  4655  xp11m  5042  funopg  5222  dffo4  5633  elunirn  5734  f1oiso  5794  canth  5796  eusvobj2  5828  acexmidlema  5833  acexmidlemb  5834  acexmidlemab  5836  acexmidlem2  5839  mpoeq123  5901  oprssdmm  6139  unielxp  6142  cnvf1o  6193  smoel  6268  tfr0dm  6290  frecabcl  6367  nnsucelsuc  6459  nntri3or  6461  nntri2  6462  nntri3  6465  nndceq  6467  nnmordi  6484  nnaordex  6495  elqsn0m  6569  qsel  6578  mapsn  6656  findcard2s  6856  undifdcss  6888  ctssdclemr  7077  nnnninf2  7091  exmidonfinlem  7149  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  exmidontriimlem3  7179  exmidontriimlem4  7180  exmidontriim  7181  pw1ne3  7186  sucpw1ne3  7188  sucpw1nel3  7189  onntri35  7193  elni2  7255  addnidpig  7277  elinp  7415  suplocexprlemdisj  7661  suplocexprlemub  7664  pitonn  7789  peano1nnnn  7793  peano2nnnn  7794  peano5nnnn  7833  sup3exmid  8852  peano5nni  8860  1nn  8868  peano2nn  8869  dfuzi  9301  uz11  9488  elfzonlteqm1  10145  frec2uzltd  10338  0tonninf  10374  1tonninf  10375  sumeq1  11296  prodeq1f  11493  ctiunct  12373  ssomct  12378  istopg  12637  fiinbas  12687  topbas  12707  epttop  12730  restbasg  12808  icnpimaex  12851  lmcvg  12857  iscnp4  12858  cncnpi  12868  cnconst2  12873  cnptoprest  12879  cnptoprest2  12880  cnpdis  12882  lmss  12886  lmff  12889  txbas  12898  eltx  12899  txcnp  12911  txlm  12919  blssps  13067  blss  13068  blssexps  13069  blssex  13070  neibl  13131  metss  13134  metrest  13146  xmettx  13150  metcnp3  13151  tgioo  13186  tgqioo  13187  bdsep2  13768  bdzfauscl  13772  bj-indeq  13811  bj-nn0suc0  13832  bj-nnelirr  13835  bj-peano4  13837  bj-inf2vnlem2  13853  bj-nn0sucALT  13860  bj-findis  13861  strcollnft  13866  sscoll2  13870  nninfsellemdc  13890  nninfsellemqall  13895