Theorem eleq2 2228

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1340   = wceq 1342  ∃wex 1479   ∈ wcel 2135

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157  df-clel 2160

This theorem is referenced by:  eleq12  2229  eleq2i  2231  eleq2d  2234  nelneq2  2266  clelsb4  2270  dvelimdc  2327  nelne1  2424  neleq2  2434  raleqf  2655  rexeqf  2656  reueq1f  2657  rmoeq1f  2658  rabeqf  2711  clel3g  2855  clel4  2857  sbcbi2  2996  sbcel2gv  3009  csbeq2  3064  sbnfc2  3100  difeq2  3229  uneq1  3264  ineq1  3311  n0i  3409  disjel  3458  exsnrex  3612  sneqr  3734  preqr1g  3740  preqr1  3742  preq12b  3744  prel12  3745  elunii  3788  eluniab  3795  ssuni  3805  elinti  3827  elintab  3829  intss1  3833  intmin  3838  intab  3847  iineq2  3877  dfiin2g  3893  breq  3978  axsep2  4095  zfauscl  4096  inuni  4128  exmidexmid  4169  ss1o0el1  4170  exmid01  4171  exmidundif  4179  exmidundifim  4180  rext  4187  intid  4196  mss  4198  opth1  4208  opeqex  4221  frforeq3  4319  frirrg  4322  limeq  4349  nsuceq0g  4390  suctr  4393  snnex  4420  uniuni  4423  iunpw  4452  ordtriexmidlem  4490  ordtriexmidlem2  4491  ordtriexmid  4492  ontriexmidim  4493  ordtri2orexmid  4494  ontr2exmid  4496  ordtri2or2exmidlem  4497  onsucelsucexmidlem  4500  onsucelsucexmid  4501  ordsucunielexmid  4502  regexmidlem1  4504  reg2exmidlema  4505  regexmid  4506  reg2exmid  4507  elirr  4512  en2lp  4525  suc11g  4528  dtruex  4530  ordsoexmid  4533  nlimsucg  4537  onintexmid  4544  reg3exmidlemwe  4550  reg3exmid  4551  peano5  4569  limom  4585  0elnn  4590  nn0eln0  4591  nnregexmid  4592  xpeq1  4612  xpeq2  4613  opthprc  4649  xp11m  5036  funopg  5216  dffo4  5627  elunirn  5728  f1oiso  5788  canth  5790  eusvobj2  5822  acexmidlema  5827  acexmidlemb  5828  acexmidlemab  5830  acexmidlem2  5833  mpoeq123  5892  oprssdmm  6131  unielxp  6134  cnvf1o  6184  smoel  6259  tfr0dm  6281  frecabcl  6358  nnsucelsuc  6450  nntri3or  6452  nntri2  6453  nntri3  6456  nndceq  6458  nnmordi  6475  nnaordex  6486  elqsn0m  6560  qsel  6569  mapsn  6647  findcard2s  6847  undifdcss  6879  ctssdclemr  7068  nnnninf2  7082  exmidonfinlem  7140  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  exmidaclem  7155  exmidontriimlem3  7170  exmidontriimlem4  7171  exmidontriim  7172  pw1ne3  7177  sucpw1ne3  7179  sucpw1nel3  7180  onntri35  7184  elni2  7246  addnidpig  7268  elinp  7406  suplocexprlemdisj  7652  suplocexprlemub  7655  pitonn  7780  peano1nnnn  7784  peano2nnnn  7785  peano5nnnn  7824  sup3exmid  8843  peano5nni  8851  1nn  8859  peano2nn  8860  dfuzi  9292  uz11  9479  elfzonlteqm1  10135  frec2uzltd  10328  0tonninf  10364  1tonninf  10365  sumeq1  11282  prodeq1f  11479  ctiunct  12310  ssomct  12315  istopg  12538  fiinbas  12588  topbas  12608  epttop  12631  restbasg  12709  icnpimaex  12752  lmcvg  12758  iscnp4  12759  cncnpi  12769  cnconst2  12774  cnptoprest  12780  cnptoprest2  12781  cnpdis  12783  lmss  12787  lmff  12790  txbas  12799  eltx  12800  txcnp  12812  txlm  12820  blssps  12968  blss  12969  blssexps  12970  blssex  12971  neibl  13032  metss  13035  metrest  13047  xmettx  13051  metcnp3  13052  tgioo  13087  tgqioo  13088  bdsep2  13603  bdzfauscl  13607  bj-indeq  13646  bj-nn0suc0  13667  bj-nnelirr  13670  bj-peano4  13672  bj-inf2vnlem2  13688  bj-nn0sucALT  13695  bj-findis  13696  strcollnft  13701  sscoll2  13705  nninfsellemdc  13724  nninfsellemqall  13729