Theorem eleq2 2302

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12  2303  eleq2i  2305  eleq2d  2308  nelneq2  2340  clelsb2  2344  dvelimdc  2413  nelne1  2510  neleq2  2520  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2811  clel3g  2960  clel4  2962  sbcbi2  3102  sbcel2gv  3115  csbeq2  3171  sbnfc2  3208  difeq2  3341  uneq1  3376  ineq1  3425  nel02  3526  n0i  3527  disjel  3579  exsnrex  3751  sneqr  3885  preqr1g  3891  preqr1  3893  preq12b  3895  prel12  3896  elunii  3940  eluniab  3947  ssuni  3957  elinti  3979  elintab  3981  intss1  3985  intmin  3990  intab  3999  iineq2  4029  dfiin2g  4045  breq  4133  axsepg  4252  sepg  4253  zfausclOLD  4255  inuni  4293  exmidexmid  4335  ss1o0el1  4336  exmid01  4337  exmidundif  4345  exmidundifim  4346  rext  4357  intid  4366  mss  4368  opth1  4378  opeqex  4392  frforeq3  4494  frirrg  4497  limeq  4524  nsuceq0g  4565  suctr  4568  snnex  4596  uniuni  4599  iunpw  4628  ordtriexmidlem  4668  ordtriexmidlem2  4669  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  ontr2exmid  4674  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  onsucelsucexmid  4679  ordsucunielexmid  4680  regexmidlem1  4682  reg2exmidlema  4683  regexmid  4684  reg2exmid  4685  elirr  4690  en2lp  4703  suc11g  4706  dtruex  4708  ordsoexmid  4711  nlimsucg  4715  onintexmid  4722  reg3exmidlemwe  4728  reg3exmid  4729  peano5  4747  limom  4763  0elnn  4768  nn0eln0  4769  nnregexmid  4770  xpeq1  4790  xpeq2  4791  opthprc  4828  xp11m  5229  funopg  5414  dffo4  5859  funopdmsn  5898  elunirn  5975  f1oiso  6035  canth  6039  eusvobj2  6074  acexmidlema  6079  acexmidlemb  6080  acexmidlemab  6082  acexmidlem2  6085  mpoeq123  6150  oprssdmm  6409  unielxp  6412  cnvf1o  6465  smoel  6576  tfr0dm  6598  frecabcl  6675  nnsucelsuc  6769  nntri3or  6771  nntri2  6772  nntri3  6775  nndceq  6777  nnmordi  6794  nnaordex  6806  elqsn0m  6882  qsel  6891  mapsnd  6976  mapsn  6978  en2m  7119  pw2f1odclem  7140  findcard2s  7200  elssdc  7215  eqsndc  7216  undifdcss  7236  fissfi  7269  2omap  7324  ctssdclemr  7458  nnnninf2  7473  exmidonfinlem  7551  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  finacn  7566  exmidaclem  7570  exmidontriimlem3  7585  exmidontriimlem4  7586  exmidontriim  7587  iftrueb01  7588  pw1ne3  7595  sucpw1ne3  7597  sucpw1nel3  7598  onntri35  7602  acnccim  7644  elni2  7687  addnidpig  7709  elinp  7847  suplocexprlemdisj  8093  suplocexprlemub  8096  pitonn  8221  peano1nnnn  8225  peano2nnnn  8226  peano5nnnn  8265  sup3exmid  9295  indval  9305  peano5nni  9316  1nn  9324  peano2nn  9325  dfuzi  9766  uz11  9960  elfzonlteqm1  10644  frec2uzltd  10860  0tonninf  10897  1tonninf  10898  hashfibclem  11303  hashf1lem2  11307  wrdsymb0  11358  lsw0  11373  swrdwrdsymbg  11457  sumeq1  12145  prodeq1f  12343  nninfctlemfo  12841  ballotfilemcdc  13280  ballotfilem7  13336  ctiunct  13388  ssomct  13393  issubm  13837  isnsg  14063  releqgg  14081  eqgex  14082  resghm  14121  ghmeql  14128  issubrg  14637  lmodfopnelem2  14770  islssm  14802  islssmg  14803  lspsneq0  14871  istopg  15242  fiinbas  15292  topbas  15310  epttop  15333  restbasg  15411  icnpimaex  15454  lmcvg  15460  iscnp4  15461  cncnpi  15471  cnconst2  15476  cnptoprest  15482  cnptoprest2  15483  cnpdis  15485  lmss  15489  lmff  15492  txbas  15501  eltx  15502  txcnp  15514  txlm  15522  blssps  15670  blss  15671  blssexps  15672  blssex  15673  neibl  15734  metss  15737  metrest  15749  xmettx  15753  metcnp3  15754  tgioo  15797  tgqioo  15798  uhgrm  16541  lpvtx  16542  incistruhgr  16553  umgrnloopv  16577  uhgredgm  16599  uhgrvtxedgiedgb  16606  upgredg2vtx  16611  uhgr2edg  16669  umgrvad2edg  16674  usgredg4  16678  uspgredg2vlem  16683  ushgredgedg  16689  subgruhgredgdm  16733  vtxd0nedgbfi  16762  1loopgrvd2fi  16768  wlk1walkdom  16822  bdsep2  17134  bdsepg  17138  bj-indeq  17177  bj-nn0suc0  17198  bj-nnelirr  17201  bj-peano4  17203  bj-inf2vnlem2  17219  bj-nn0sucALT  17226  bj-findis  17227  strcollnft  17232  sscoll2  17236  nninfsellemdc  17276  nninfsellemqall  17281  nnnninfex  17288