Theorem eleq2 2234

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1346   = wceq 1348  ∃wex 1485   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleq12  2235  eleq2i  2237  eleq2d  2240  nelneq2  2272  clelsb2  2276  dvelimdc  2333  nelne1  2430  neleq2  2440  raleqf  2661  rexeqf  2662  reueq1f  2663  rmoeq1f  2664  rabeqf  2720  clel3g  2864  clel4  2866  sbcbi2  3005  sbcel2gv  3018  csbeq2  3073  sbnfc2  3109  difeq2  3239  uneq1  3274  ineq1  3321  nel02  3419  n0i  3420  disjel  3469  exsnrex  3625  sneqr  3747  preqr1g  3753  preqr1  3755  preq12b  3757  prel12  3758  elunii  3801  eluniab  3808  ssuni  3818  elinti  3840  elintab  3842  intss1  3846  intmin  3851  intab  3860  iineq2  3890  dfiin2g  3906  breq  3991  axsep2  4108  zfauscl  4109  inuni  4141  exmidexmid  4182  ss1o0el1  4183  exmid01  4184  exmidundif  4192  exmidundifim  4193  rext  4200  intid  4209  mss  4211  opth1  4221  opeqex  4234  frforeq3  4332  frirrg  4335  limeq  4362  nsuceq0g  4403  suctr  4406  snnex  4433  uniuni  4436  iunpw  4465  ordtriexmidlem  4503  ordtriexmidlem2  4504  ordtriexmid  4505  ontriexmidim  4506  ordtri2orexmid  4507  ontr2exmid  4509  ordtri2or2exmidlem  4510  onsucelsucexmidlem  4513  onsucelsucexmid  4514  ordsucunielexmid  4515  regexmidlem1  4517  reg2exmidlema  4518  regexmid  4519  reg2exmid  4520  elirr  4525  en2lp  4538  suc11g  4541  dtruex  4543  ordsoexmid  4546  nlimsucg  4550  onintexmid  4557  reg3exmidlemwe  4563  reg3exmid  4564  peano5  4582  limom  4598  0elnn  4603  nn0eln0  4604  nnregexmid  4605  xpeq1  4625  xpeq2  4626  opthprc  4662  xp11m  5049  funopg  5232  dffo4  5644  elunirn  5745  f1oiso  5805  canth  5807  eusvobj2  5839  acexmidlema  5844  acexmidlemb  5845  acexmidlemab  5847  acexmidlem2  5850  mpoeq123  5912  oprssdmm  6150  unielxp  6153  cnvf1o  6204  smoel  6279  tfr0dm  6301  frecabcl  6378  nnsucelsuc  6470  nntri3or  6472  nntri2  6473  nntri3  6476  nndceq  6478  nnmordi  6495  nnaordex  6507  elqsn0m  6581  qsel  6590  mapsn  6668  findcard2s  6868  undifdcss  6900  ctssdclemr  7089  nnnninf2  7103  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  exmidontriimlem3  7200  exmidontriimlem4  7201  exmidontriim  7202  pw1ne3  7207  sucpw1ne3  7209  sucpw1nel3  7210  onntri35  7214  elni2  7276  addnidpig  7298  elinp  7436  suplocexprlemdisj  7682  suplocexprlemub  7685  pitonn  7810  peano1nnnn  7814  peano2nnnn  7815  peano5nnnn  7854  sup3exmid  8873  peano5nni  8881  1nn  8889  peano2nn  8890  dfuzi  9322  uz11  9509  elfzonlteqm1  10166  frec2uzltd  10359  0tonninf  10395  1tonninf  10396  sumeq1  11318  prodeq1f  11515  ctiunct  12395  ssomct  12400  issubm  12695  istopg  12791  fiinbas  12841  topbas  12861  epttop  12884  restbasg  12962  icnpimaex  13005  lmcvg  13011  iscnp4  13012  cncnpi  13022  cnconst2  13027  cnptoprest  13033  cnptoprest2  13034  cnpdis  13036  lmss  13040  lmff  13043  txbas  13052  eltx  13053  txcnp  13065  txlm  13073  blssps  13221  blss  13222  blssexps  13223  blssex  13224  neibl  13285  metss  13288  metrest  13300  xmettx  13304  metcnp3  13305  tgioo  13340  tgqioo  13341  bdsep2  13921  bdzfauscl  13925  bj-indeq  13964  bj-nn0suc0  13985  bj-nnelirr  13988  bj-peano4  13990  bj-inf2vnlem2  14006  bj-nn0sucALT  14013  bj-findis  14014  strcollnft  14019  sscoll2  14023  nninfsellemdc  14043  nninfsellemqall  14048