Theorem eleq2 2295

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2202

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12  2296  eleq2i  2298  eleq2d  2301  nelneq2  2333  clelsb2  2337  dvelimdc  2396  nelne1  2493  neleq2  2503  raleqf  2727  rexeqf  2728  reueq1f  2729  rmoeq1f  2730  rabeqf  2793  clel3g  2941  clel4  2943  sbcbi2  3083  sbcel2gv  3096  csbeq2  3152  sbnfc2  3189  difeq2  3321  uneq1  3356  ineq1  3403  nel02  3501  n0i  3502  disjel  3551  exsnrex  3715  sneqr  3848  preqr1g  3854  preqr1  3856  preq12b  3858  prel12  3859  elunii  3903  eluniab  3910  ssuni  3920  elinti  3942  elintab  3944  intss1  3948  intmin  3953  intab  3962  iineq2  3992  dfiin2g  4008  breq  4095  axsep2  4213  zfauscl  4214  inuni  4250  exmidexmid  4292  ss1o0el1  4293  exmid01  4294  exmidundif  4302  exmidundifim  4303  rext  4313  intid  4322  mss  4324  opth1  4334  opeqex  4348  frforeq3  4450  frirrg  4453  limeq  4480  nsuceq0g  4521  suctr  4524  snnex  4551  uniuni  4554  iunpw  4583  ordtriexmidlem  4623  ordtriexmidlem2  4624  ordtriexmid  4625  ontriexmidim  4626  ordtri2orexmid  4627  ontr2exmid  4629  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  onsucelsucexmid  4634  ordsucunielexmid  4635  regexmidlem1  4637  reg2exmidlema  4638  regexmid  4639  reg2exmid  4640  elirr  4645  en2lp  4658  suc11g  4661  dtruex  4663  ordsoexmid  4666  nlimsucg  4670  onintexmid  4677  reg3exmidlemwe  4683  reg3exmid  4684  peano5  4702  limom  4718  0elnn  4723  nn0eln0  4724  nnregexmid  4725  xpeq1  4745  xpeq2  4746  opthprc  4783  xp11m  5182  funopg  5367  dffo4  5803  funopdmsn  5842  elunirn  5917  f1oiso  5977  canth  5979  eusvobj2  6014  acexmidlema  6019  acexmidlemb  6020  acexmidlemab  6022  acexmidlem2  6025  mpoeq123  6090  oprssdmm  6343  unielxp  6346  cnvf1o  6399  smoel  6509  tfr0dm  6531  frecabcl  6608  nnsucelsuc  6702  nntri3or  6704  nntri2  6705  nntri3  6708  nndceq  6710  nnmordi  6727  nnaordex  6739  elqsn0m  6815  qsel  6824  mapsn  6902  en2m  7042  pw2f1odclem  7063  findcard2s  7122  elssdc  7137  eqsndc  7138  undifdcss  7158  ctssdclemr  7354  nnnninf2  7369  exmidonfinlem  7447  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  finacn  7462  exmidaclem  7466  exmidontriimlem3  7481  exmidontriimlem4  7482  exmidontriim  7483  iftrueb01  7484  pw1ne3  7491  sucpw1ne3  7493  sucpw1nel3  7494  onntri35  7498  acnccim  7534  elni2  7577  addnidpig  7599  elinp  7737  suplocexprlemdisj  7983  suplocexprlemub  7986  pitonn  8111  peano1nnnn  8115  peano2nnnn  8116  peano5nnnn  8155  sup3exmid  9179  peano5nni  9188  1nn  9196  peano2nn  9197  dfuzi  9634  uz11  9823  elfzonlteqm1  10501  frec2uzltd  10711  0tonninf  10748  1tonninf  10749  wrdsymb0  11195  lsw0  11210  swrdwrdsymbg  11294  sumeq1  11978  prodeq1f  12176  nninfctlemfo  12674  ctiunct  13124  ssomct  13129  issubm  13618  isnsg  13852  releqgg  13870  eqgex  13871  resghm  13910  ghmeql  13917  issubrg  14299  lmodfopnelem2  14404  islssm  14436  islssmg  14437  lspsneq0  14505  istopg  14793  fiinbas  14843  topbas  14861  epttop  14884  restbasg  14962  icnpimaex  15005  lmcvg  15011  iscnp4  15012  cncnpi  15022  cnconst2  15027  cnptoprest  15033  cnptoprest2  15034  cnpdis  15036  lmss  15040  lmff  15043  txbas  15052  eltx  15053  txcnp  15065  txlm  15073  blssps  15221  blss  15222  blssexps  15223  blssex  15224  neibl  15285  metss  15288  metrest  15300  xmettx  15304  metcnp3  15305  tgioo  15348  tgqioo  15349  uhgrm  16002  lpvtx  16003  incistruhgr  16014  umgrnloopv  16038  uhgredgm  16060  uhgrvtxedgiedgb  16067  upgredg2vtx  16072  uhgr2edg  16130  umgrvad2edg  16135  usgredg4  16139  uspgredg2vlem  16144  ushgredgedg  16150  subgruhgredgdm  16194  vtxd0nedgbfi  16223  1loopgrvd2fi  16229  wlk1walkdom  16283  bdsep2  16585  bdzfauscl  16589  bj-indeq  16628  bj-nn0suc0  16649  bj-nnelirr  16652  bj-peano4  16654  bj-inf2vnlem2  16670  bj-nn0sucALT  16677  bj-findis  16678  strcollnft  16683  sscoll2  16687  2omap  16698  nninfsellemdc  16719  nninfsellemqall  16724  nnnninfex  16731