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  6575  tfr0dm  6597  frecabcl  6674  nnsucelsuc  6768  nntri3or  6770  nntri2  6771  nntri3  6774  nndceq  6776  nnmordi  6793  nnaordex  6805  elqsn0m  6881  qsel  6890  mapsnd  6974  mapsn  6976  en2m  7117  pw2f1odclem  7138  findcard2s  7198  elssdc  7213  eqsndc  7214  undifdcss  7234  fissfi  7267  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  9767  uz11  9961  elfzonlteqm1  10645  frec2uzltd  10861  0tonninf  10898  1tonninf  10899  hashfibclem  11304  hashf1lem2  11308  wrdsymb0  11359  lsw0  11374  swrdwrdsymbg  11458  sumeq1  12146  prodeq1f  12344  nninfctlemfo  12842  ballotfilemcdc  13281  ballotfilem7  13337  ctiunct  13389  ssomct  13394  issubm  13838  isnsg  14064  releqgg  14082  eqgex  14083  resghm  14122  ghmeql  14129  issubrg  14638  lmodfopnelem2  14771  islssm  14803  islssmg  14804  lspsneq0  14872  istopg  15225  fiinbas  15275  topbas  15293  epttop  15316  restbasg  15394  icnpimaex  15437  lmcvg  15443  iscnp4  15444  cncnpi  15454  cnconst2  15459  cnptoprest  15465  cnptoprest2  15466  cnpdis  15468  lmss  15472  lmff  15475  txbas  15484  eltx  15485  txcnp  15497  txlm  15505  blssps  15653  blss  15654  blssexps  15655  blssex  15656  neibl  15717  metss  15720  metrest  15732  xmettx  15736  metcnp3  15737  tgioo  15780  tgqioo  15781  uhgrm  16524  lpvtx  16525  incistruhgr  16536  umgrnloopv  16560  uhgredgm  16582  uhgrvtxedgiedgb  16589  upgredg2vtx  16594  uhgr2edg  16652  umgrvad2edg  16657  usgredg4  16661  uspgredg2vlem  16666  ushgredgedg  16672  subgruhgredgdm  16716  vtxd0nedgbfi  16745  1loopgrvd2fi  16751  wlk1walkdom  16805  bdsep2  17117  bdsepg  17121  bj-indeq  17160  bj-nn0suc0  17181  bj-nnelirr  17184  bj-peano4  17186  bj-inf2vnlem2  17202  bj-nn0sucALT  17209  bj-findis  17210  strcollnft  17215  sscoll2  17219  nninfsellemdc  17259  nninfsellemqall  17264  nnnninfex  17271