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  3837  preqr1g  3843  preqr1  3845  preq12b  3847  prel12  3848  elunii  3892  eluniab  3899  ssuni  3909  elinti  3931  elintab  3933  intss1  3937  intmin  3942  intab  3951  iineq2  3981  dfiin2g  3997  breq  4084  axsep2  4202  zfauscl  4203  inuni  4238  exmidexmid  4279  ss1o0el1  4280  exmid01  4281  exmidundif  4289  exmidundifim  4290  rext  4300  intid  4309  mss  4311  opth1  4321  opeqex  4335  frforeq3  4437  frirrg  4440  limeq  4467  nsuceq0g  4508  suctr  4511  snnex  4538  uniuni  4541  iunpw  4570  ordtriexmidlem  4610  ordtriexmidlem2  4611  ordtriexmid  4612  ontriexmidim  4613  ordtri2orexmid  4614  ontr2exmid  4616  ordtri2or2exmidlem  4617  onsucelsucexmidlem  4620  onsucelsucexmid  4621  ordsucunielexmid  4622  regexmidlem1  4624  reg2exmidlema  4625  regexmid  4626  reg2exmid  4627  elirr  4632  en2lp  4645  suc11g  4648  dtruex  4650  ordsoexmid  4653  nlimsucg  4657  onintexmid  4664  reg3exmidlemwe  4670  reg3exmid  4671  peano5  4689  limom  4705  0elnn  4710  nn0eln0  4711  nnregexmid  4712  xpeq1  4732  xpeq2  4733  opthprc  4769  xp11m  5166  funopg  5351  dffo4  5782  funopdmsn  5818  elunirn  5889  f1oiso  5949  canth  5951  eusvobj2  5986  acexmidlema  5991  acexmidlemb  5992  acexmidlemab  5994  acexmidlem2  5997  mpoeq123  6062  oprssdmm  6315  unielxp  6318  cnvf1o  6369  smoel  6444  tfr0dm  6466  frecabcl  6543  nnsucelsuc  6635  nntri3or  6637  nntri2  6638  nntri3  6641  nndceq  6643  nnmordi  6660  nnaordex  6672  elqsn0m  6748  qsel  6757  mapsn  6835  en2m  6972  pw2f1odclem  6991  findcard2s  7048  undifdcss  7081  ctssdclemr  7275  nnnninf2  7290  exmidonfinlem  7367  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  finacn  7382  exmidaclem  7386  exmidontriimlem3  7401  exmidontriimlem4  7402  exmidontriim  7403  iftrueb01  7404  pw1ne3  7411  sucpw1ne3  7413  sucpw1nel3  7414  onntri35  7418  acnccim  7454  elni2  7497  addnidpig  7519  elinp  7657  suplocexprlemdisj  7903  suplocexprlemub  7906  pitonn  8031  peano1nnnn  8035  peano2nnnn  8036  peano5nnnn  8075  sup3exmid  9100  peano5nni  9109  1nn  9117  peano2nn  9118  dfuzi  9553  uz11  9741  elfzonlteqm1  10411  frec2uzltd  10620  0tonninf  10657  1tonninf  10658  wrdsymb0  11099  lsw0  11114  swrdwrdsymbg  11191  sumeq1  11861  prodeq1f  12058  nninfctlemfo  12556  ctiunct  13006  ssomct  13011  issubm  13500  isnsg  13734  releqgg  13752  eqgex  13753  resghm  13792  ghmeql  13799  issubrg  14179  lmodfopnelem2  14283  islssm  14315  islssmg  14316  lspsneq0  14384  istopg  14667  fiinbas  14717  topbas  14735  epttop  14758  restbasg  14836  icnpimaex  14879  lmcvg  14885  iscnp4  14886  cncnpi  14896  cnconst2  14901  cnptoprest  14907  cnptoprest2  14908  cnpdis  14910  lmss  14914  lmff  14917  txbas  14926  eltx  14927  txcnp  14939  txlm  14947  blssps  15095  blss  15096  blssexps  15097  blssex  15098  neibl  15159  metss  15162  metrest  15174  xmettx  15178  metcnp3  15179  tgioo  15222  tgqioo  15223  uhgrm  15872  lpvtx  15873  incistruhgr  15884  umgrnloopv  15908  uhgredgm  15928  uhgrvtxedgiedgb  15935  upgredg2vtx  15940  uhgr2edg  15998  umgrvad2edg  16003  usgredg4  16007  uspgredg2vlem  16012  ushgredgedg  16018  bdsep2  16207  bdzfauscl  16211  bj-indeq  16250  bj-nn0suc0  16271  bj-nnelirr  16274  bj-peano4  16276  bj-inf2vnlem2  16292  bj-nn0sucALT  16299  bj-findis  16300  strcollnft  16305  sscoll2  16309  2omap  16318  nninfsellemdc  16335  nninfsellemqall  16340  nnnninfex  16347