Theorem eleq2 2201

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1329   = wceq 1331  ∃wex 1468   ∈ wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  eleq12  2202  eleq2i  2204  eleq2d  2207  nelneq2  2239  clelsb4  2243  dvelimdc  2299  nelne1  2396  neleq2  2406  raleqf  2620  rexeqf  2621  reueq1f  2622  rmoeq1f  2623  rabeqf  2671  clel3g  2814  clel4  2816  sbcbi2  2954  sbcel2gv  2967  csbeq2  3021  sbnfc2  3055  difeq2  3183  uneq1  3218  ineq1  3265  n0i  3363  disjel  3412  exsnrex  3561  sneqr  3682  preqr1g  3688  preqr1  3690  preq12b  3692  prel12  3693  elunii  3736  eluniab  3743  ssuni  3753  elinti  3775  elintab  3777  intss1  3781  intmin  3786  intab  3795  iineq2  3825  dfiin2g  3841  breq  3926  axsep2  4042  zfauscl  4043  inuni  4075  exmidexmid  4115  exmid01  4116  exmidundif  4124  exmidundifim  4125  rext  4132  intid  4141  mss  4143  opth1  4153  opeqex  4166  frforeq3  4264  frirrg  4267  limeq  4294  nsuceq0g  4335  suctr  4338  snnex  4364  uniuni  4367  iunpw  4396  ordtriexmidlem  4430  ordtriexmidlem2  4431  ordtriexmid  4432  ordtri2orexmid  4433  ontr2exmid  4435  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  onsucelsucexmid  4440  ordsucunielexmid  4441  regexmidlem1  4443  reg2exmidlema  4444  regexmid  4445  reg2exmid  4446  elirr  4451  en2lp  4464  suc11g  4467  dtruex  4469  ordsoexmid  4472  nlimsucg  4476  onintexmid  4482  reg3exmidlemwe  4488  reg3exmid  4489  peano5  4507  limom  4522  0elnn  4527  nn0eln0  4528  nnregexmid  4529  xpeq1  4548  xpeq2  4549  opthprc  4585  xp11m  4972  funopg  5152  dffo4  5561  elunirn  5660  f1oiso  5720  eusvobj2  5753  acexmidlema  5758  acexmidlemb  5759  acexmidlemab  5761  acexmidlem2  5764  mpoeq123  5823  oprssdmm  6062  unielxp  6065  cnvf1o  6115  smoel  6190  tfr0dm  6212  frecabcl  6289  nnsucelsuc  6380  nntri3or  6382  nntri2  6383  nntri3  6386  nndceq  6388  nnmordi  6405  nnaordex  6416  elqsn0m  6490  qsel  6499  mapsn  6577  findcard2s  6777  undifdcss  6804  ctssdclemr  6990  exmidonfinlem  7042  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  exmidaclem  7057  elni2  7115  addnidpig  7137  elinp  7275  suplocexprlemdisj  7521  suplocexprlemub  7524  pitonn  7649  peano1nnnn  7653  peano2nnnn  7654  peano5nnnn  7693  sup3exmid  8708  peano5nni  8716  1nn  8724  peano2nn  8725  dfuzi  9154  uz11  9341  elfzonlteqm1  9980  frec2uzltd  10169  0tonninf  10205  1tonninf  10206  sumeq1  11117  prodeq1f  11314  ctiunct  11942  istopg  12155  fiinbas  12205  topbas  12225  epttop  12248  restbasg  12326  icnpimaex  12369  lmcvg  12375  iscnp4  12376  cncnpi  12386  cnconst2  12391  cnptoprest  12397  cnptoprest2  12398  cnpdis  12400  lmss  12404  lmff  12407  txbas  12416  eltx  12417  txcnp  12429  txlm  12437  blssps  12585  blss  12586  blssexps  12587  blssex  12588  neibl  12649  metss  12652  metrest  12664  xmettx  12668  metcnp3  12669  tgioo  12704  tgqioo  12705  bdsep2  13073  bdzfauscl  13077  bj-indeq  13116  bj-nn0suc0  13137  bj-nnelirr  13140  bj-peano4  13142  bj-inf2vnlem2  13158  bj-nn0sucALT  13165  bj-findis  13166  nninfsellemdc  13195  nninfsellemqall  13200