Theorem eleq2 2293

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1393   = wceq 1395  ∃wex 1538   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12  2294  eleq2i  2296  eleq2d  2299  nelneq2  2331  clelsb2  2335  dvelimdc  2393  nelne1  2490  neleq2  2500  raleqf  2724  rexeqf  2725  reueq1f  2726  rmoeq1f  2727  rabeqf  2789  clel3g  2937  clel4  2939  sbcbi2  3079  sbcel2gv  3092  csbeq2  3148  sbnfc2  3185  difeq2  3316  uneq1  3351  ineq1  3398  nel02  3496  n0i  3497  disjel  3546  exsnrex  3708  sneqr  3838  preqr1g  3844  preqr1  3846  preq12b  3848  prel12  3849  elunii  3893  eluniab  3900  ssuni  3910  elinti  3932  elintab  3934  intss1  3938  intmin  3943  intab  3952  iineq2  3982  dfiin2g  3998  breq  4085  axsep2  4203  zfauscl  4204  inuni  4239  exmidexmid  4280  ss1o0el1  4281  exmid01  4282  exmidundif  4290  exmidundifim  4291  rext  4301  intid  4310  mss  4312  opth1  4322  opeqex  4336  frforeq3  4438  frirrg  4441  limeq  4468  nsuceq0g  4509  suctr  4512  snnex  4539  uniuni  4542  iunpw  4571  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  ontr2exmid  4617  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  onsucelsucexmid  4622  ordsucunielexmid  4623  regexmidlem1  4625  reg2exmidlema  4626  regexmid  4627  reg2exmid  4628  elirr  4633  en2lp  4646  suc11g  4649  dtruex  4651  ordsoexmid  4654  nlimsucg  4658  onintexmid  4665  reg3exmidlemwe  4671  reg3exmid  4672  peano5  4690  limom  4706  0elnn  4711  nn0eln0  4712  nnregexmid  4713  xpeq1  4733  xpeq2  4734  opthprc  4770  xp11m  5167  funopg  5352  dffo4  5785  funopdmsn  5823  elunirn  5896  f1oiso  5956  canth  5958  eusvobj2  5993  acexmidlema  5998  acexmidlemb  5999  acexmidlemab  6001  acexmidlem2  6004  mpoeq123  6069  oprssdmm  6323  unielxp  6326  cnvf1o  6377  smoel  6452  tfr0dm  6474  frecabcl  6551  nnsucelsuc  6645  nntri3or  6647  nntri2  6648  nntri3  6651  nndceq  6653  nnmordi  6670  nnaordex  6682  elqsn0m  6758  qsel  6767  mapsn  6845  en2m  6982  pw2f1odclem  7003  findcard2s  7060  elssdc  7075  eqsndc  7076  undifdcss  7096  ctssdclemr  7290  nnnninf2  7305  exmidonfinlem  7382  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  finacn  7397  exmidaclem  7401  exmidontriimlem3  7416  exmidontriimlem4  7417  exmidontriim  7418  iftrueb01  7419  pw1ne3  7426  sucpw1ne3  7428  sucpw1nel3  7429  onntri35  7433  acnccim  7469  elni2  7512  addnidpig  7534  elinp  7672  suplocexprlemdisj  7918  suplocexprlemub  7921  pitonn  8046  peano1nnnn  8050  peano2nnnn  8051  peano5nnnn  8090  sup3exmid  9115  peano5nni  9124  1nn  9132  peano2nn  9133  dfuzi  9568  uz11  9757  elfzonlteqm1  10428  frec2uzltd  10637  0tonninf  10674  1tonninf  10675  wrdsymb0  11117  lsw0  11132  swrdwrdsymbg  11211  sumeq1  11881  prodeq1f  12078  nninfctlemfo  12576  ctiunct  13026  ssomct  13031  issubm  13520  isnsg  13754  releqgg  13772  eqgex  13773  resghm  13812  ghmeql  13819  issubrg  14200  lmodfopnelem2  14304  islssm  14336  islssmg  14337  lspsneq0  14405  istopg  14688  fiinbas  14738  topbas  14756  epttop  14779  restbasg  14857  icnpimaex  14900  lmcvg  14906  iscnp4  14907  cncnpi  14917  cnconst2  14922  cnptoprest  14928  cnptoprest2  14929  cnpdis  14931  lmss  14935  lmff  14938  txbas  14947  eltx  14948  txcnp  14960  txlm  14968  blssps  15116  blss  15117  blssexps  15118  blssex  15119  neibl  15180  metss  15183  metrest  15195  xmettx  15199  metcnp3  15200  tgioo  15243  tgqioo  15244  uhgrm  15893  lpvtx  15894  incistruhgr  15905  umgrnloopv  15929  uhgredgm  15949  uhgrvtxedgiedgb  15956  upgredg2vtx  15961  uhgr2edg  16019  umgrvad2edg  16024  usgredg4  16028  uspgredg2vlem  16033  ushgredgedg  16039  wlk1walkdom  16100  bdsep2  16304  bdzfauscl  16308  bj-indeq  16347  bj-nn0suc0  16368  bj-nnelirr  16371  bj-peano4  16373  bj-inf2vnlem2  16389  bj-nn0sucALT  16396  bj-findis  16397  strcollnft  16402  sscoll2  16406  2omap  16418  nninfsellemdc  16436  nninfsellemqall  16441  nnnninfex  16448