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  4132  axsepg  4250  sepg  4251  zfausclOLD  4253  inuni  4291  exmidexmid  4333  ss1o0el1  4334  exmid01  4335  exmidundif  4343  exmidundifim  4344  rext  4355  intid  4364  mss  4366  opth1  4376  opeqex  4390  frforeq3  4492  frirrg  4495  limeq  4522  nsuceq0g  4563  suctr  4566  snnex  4594  uniuni  4597  iunpw  4626  ordtriexmidlem  4666  ordtriexmidlem2  4667  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  ontr2exmid  4672  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  onsucelsucexmid  4677  ordsucunielexmid  4678  regexmidlem1  4680  reg2exmidlema  4681  regexmid  4682  reg2exmid  4683  elirr  4688  en2lp  4701  suc11g  4704  dtruex  4706  ordsoexmid  4709  nlimsucg  4713  onintexmid  4720  reg3exmidlemwe  4726  reg3exmid  4727  peano5  4745  limom  4761  0elnn  4766  nn0eln0  4767  nnregexmid  4768  xpeq1  4788  xpeq2  4789  opthprc  4826  xp11m  5226  funopg  5411  dffo4  5856  funopdmsn  5895  elunirn  5972  f1oiso  6032  canth  6036  eusvobj2  6071  acexmidlema  6076  acexmidlemb  6077  acexmidlemab  6079  acexmidlem2  6082  mpoeq123  6147  oprssdmm  6405  unielxp  6408  cnvf1o  6461  smoel  6571  tfr0dm  6593  frecabcl  6670  nnsucelsuc  6764  nntri3or  6766  nntri2  6767  nntri3  6770  nndceq  6772  nnmordi  6789  nnaordex  6801  elqsn0m  6877  qsel  6886  mapsnd  6970  mapsn  6972  en2m  7113  pw2f1odclem  7134  findcard2s  7194  elssdc  7209  eqsndc  7210  undifdcss  7230  fissfi  7263  2omap  7319  ctssdclemr  7453  nnnninf2  7468  exmidonfinlem  7546  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  finacn  7561  exmidaclem  7565  exmidontriimlem3  7580  exmidontriimlem4  7581  exmidontriim  7582  iftrueb01  7583  pw1ne3  7590  sucpw1ne3  7592  sucpw1nel3  7593  onntri35  7597  acnccim  7639  elni2  7682  addnidpig  7704  elinp  7842  suplocexprlemdisj  8088  suplocexprlemub  8091  pitonn  8216  peano1nnnn  8220  peano2nnnn  8221  peano5nnnn  8260  sup3exmid  9290  indval  9299  peano5nni  9310  1nn  9318  peano2nn  9319  dfuzi  9761  uz11  9955  elfzonlteqm1  10639  frec2uzltd  10855  0tonninf  10892  1tonninf  10893  hashfibclem  11298  hashf1lem2  11302  wrdsymb0  11353  lsw0  11368  swrdwrdsymbg  11452  sumeq1  12140  prodeq1f  12338  nninfctlemfo  12836  ballotfilemcdc  13275  ballotfilem7  13331  ctiunct  13383  ssomct  13388  issubm  13832  isnsg  14058  releqgg  14076  eqgex  14077  resghm  14116  ghmeql  14123  issubrg  14613  lmodfopnelem2  14746  islssm  14778  islssmg  14779  lspsneq0  14847  istopg  15191  fiinbas  15241  topbas  15259  epttop  15282  restbasg  15360  icnpimaex  15403  lmcvg  15409  iscnp4  15410  cncnpi  15420  cnconst2  15425  cnptoprest  15431  cnptoprest2  15432  cnpdis  15434  lmss  15438  lmff  15441  txbas  15450  eltx  15451  txcnp  15463  txlm  15471  blssps  15619  blss  15620  blssexps  15621  blssex  15622  neibl  15683  metss  15686  metrest  15698  xmettx  15702  metcnp3  15703  tgioo  15746  tgqioo  15747  uhgrm  16485  lpvtx  16486  incistruhgr  16497  umgrnloopv  16521  uhgredgm  16543  uhgrvtxedgiedgb  16550  upgredg2vtx  16555  uhgr2edg  16613  umgrvad2edg  16618  usgredg4  16622  uspgredg2vlem  16627  ushgredgedg  16633  subgruhgredgdm  16677  vtxd0nedgbfi  16706  1loopgrvd2fi  16712  wlk1walkdom  16766  bdsep2  17078  bdsepg  17082  bj-indeq  17121  bj-nn0suc0  17142  bj-nnelirr  17145  bj-peano4  17147  bj-inf2vnlem2  17163  bj-nn0sucALT  17170  bj-findis  17171  strcollnft  17176  sscoll2  17180  nninfsellemdc  17219  nninfsellemqall  17224  nnnninfex  17231