Theorem eleq2 2239

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 2169	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1556	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	anbi2d 464	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
5	4	exbidv 1823	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴) ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵)))
6		df-clel 2171	. 2 ⊢ (𝐶 ∈ 𝐴 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴))
7		df-clel 2171	. 2 ⊢ (𝐶 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1351   = wceq 1353  ∃wex 1490   ∈ wcel 2146

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-clel 2171

This theorem is referenced by:  eleq12  2240  eleq2i  2242  eleq2d  2245  nelneq2  2277  clelsb2  2281  dvelimdc  2338  nelne1  2435  neleq2  2445  raleqf  2666  rexeqf  2667  reueq1f  2668  rmoeq1f  2669  rabeqf  2725  clel3g  2869  clel4  2871  sbcbi2  3011  sbcel2gv  3024  csbeq2  3079  sbnfc2  3115  difeq2  3245  uneq1  3280  ineq1  3327  nel02  3425  n0i  3426  disjel  3475  exsnrex  3631  sneqr  3756  preqr1g  3762  preqr1  3764  preq12b  3766  prel12  3767  elunii  3810  eluniab  3817  ssuni  3827  elinti  3849  elintab  3851  intss1  3855  intmin  3860  intab  3869  iineq2  3899  dfiin2g  3915  breq  4000  axsep2  4117  zfauscl  4118  inuni  4150  exmidexmid  4191  ss1o0el1  4192  exmid01  4193  exmidundif  4201  exmidundifim  4202  rext  4209  intid  4218  mss  4220  opth1  4230  opeqex  4243  frforeq3  4341  frirrg  4344  limeq  4371  nsuceq0g  4412  suctr  4415  snnex  4442  uniuni  4445  iunpw  4474  ordtriexmidlem  4512  ordtriexmidlem2  4513  ordtriexmid  4514  ontriexmidim  4515  ordtri2orexmid  4516  ontr2exmid  4518  ordtri2or2exmidlem  4519  onsucelsucexmidlem  4522  onsucelsucexmid  4523  ordsucunielexmid  4524  regexmidlem1  4526  reg2exmidlema  4527  regexmid  4528  reg2exmid  4529  elirr  4534  en2lp  4547  suc11g  4550  dtruex  4552  ordsoexmid  4555  nlimsucg  4559  onintexmid  4566  reg3exmidlemwe  4572  reg3exmid  4573  peano5  4591  limom  4607  0elnn  4612  nn0eln0  4613  nnregexmid  4614  xpeq1  4634  xpeq2  4635  opthprc  4671  xp11m  5059  funopg  5242  dffo4  5656  elunirn  5757  f1oiso  5817  canth  5819  eusvobj2  5851  acexmidlema  5856  acexmidlemb  5857  acexmidlemab  5859  acexmidlem2  5862  mpoeq123  5924  oprssdmm  6162  unielxp  6165  cnvf1o  6216  smoel  6291  tfr0dm  6313  frecabcl  6390  nnsucelsuc  6482  nntri3or  6484  nntri2  6485  nntri3  6488  nndceq  6490  nnmordi  6507  nnaordex  6519  elqsn0m  6593  qsel  6602  mapsn  6680  findcard2s  6880  undifdcss  6912  ctssdclemr  7101  nnnninf2  7115  exmidonfinlem  7182  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  exmidaclem  7197  exmidontriimlem3  7212  exmidontriimlem4  7213  exmidontriim  7214  pw1ne3  7219  sucpw1ne3  7221  sucpw1nel3  7222  onntri35  7226  elni2  7288  addnidpig  7310  elinp  7448  suplocexprlemdisj  7694  suplocexprlemub  7697  pitonn  7822  peano1nnnn  7826  peano2nnnn  7827  peano5nnnn  7866  sup3exmid  8885  peano5nni  8893  1nn  8901  peano2nn  8902  dfuzi  9334  uz11  9521  elfzonlteqm1  10178  frec2uzltd  10371  0tonninf  10407  1tonninf  10408  sumeq1  11329  prodeq1f  11526  ctiunct  12406  ssomct  12411  issubm  12724  istopg  13066  fiinbas  13116  topbas  13136  epttop  13159  restbasg  13237  icnpimaex  13280  lmcvg  13286  iscnp4  13287  cncnpi  13297  cnconst2  13302  cnptoprest  13308  cnptoprest2  13309  cnpdis  13311  lmss  13315  lmff  13318  txbas  13327  eltx  13328  txcnp  13340  txlm  13348  blssps  13496  blss  13497  blssexps  13498  blssex  13499  neibl  13560  metss  13563  metrest  13575  xmettx  13579  metcnp3  13580  tgioo  13615  tgqioo  13616  bdsep2  14196  bdzfauscl  14200  bj-indeq  14239  bj-nn0suc0  14260  bj-nnelirr  14263  bj-peano4  14265  bj-inf2vnlem2  14281  bj-nn0sucALT  14288  bj-findis  14289  strcollnft  14294  sscoll2  14298  nninfsellemdc  14318  nninfsellemqall  14323