ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleq2 GIF version

Theorem eleq2 2117
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.
StepHypRef Expression
1 dfcleq 2050 . . . . . 6 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 117 . . . . 5 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1466 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
43anbi2d 445 . . 3 (𝐴 = 𝐵 → ((𝑥 = 𝐶𝑥𝐴) ↔ (𝑥 = 𝐶𝑥𝐵)))
54exbidv 1722 . 2 (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2052 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2052 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73bitr4g 216 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102  wal 1257   = wceq 1259  wex 1397  wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  eleq12  2118  eleq2i  2120  eleq2d  2123  nelneq2  2155  clelsb4  2159  dvelimdc  2213  nelne1  2310  neleq2  2319  raleqf  2518  rexeqf  2519  reueq1f  2520  rmoeq1f  2521  rabeqf  2567  clel3g  2700  clel4  2702  sbcbi2  2835  sbcel2gv  2848  sbnfc2  2933  difeq2  3083  uneq1  3117  ineq1  3158  n0i  3256  disjel  3301  exsnrex  3440  sneqr  3558  preqr1g  3564  preqr1  3566  preq12b  3568  prel12  3569  elunii  3612  eluniab  3619  ssuni  3629  elinti  3651  elintab  3653  intss1  3657  intmin  3662  intab  3671  iineq2  3701  dfiin2g  3717  breq  3793  axsep2  3903  zfauscl  3904  inuni  3936  rext  3978  intid  3987  mss  3989  opth1  4000  opeqex  4013  frforeq3  4111  frirrg  4114  limeq  4141  nsuceq0g  4182  suctr  4185  snnex  4208  uniuni  4210  iunpw  4238  ordtriexmidlem  4272  ordtriexmidlem2  4273  ordtriexmid  4274  ordtri2orexmid  4275  ontr2exmid  4277  ordtri2or2exmidlem  4278  onsucelsucexmidlem  4281  onsucelsucexmid  4282  ordsucunielexmid  4283  regexmidlem1  4285  reg2exmidlema  4286  regexmid  4287  reg2exmid  4288  elirr  4293  en2lp  4305  suc11g  4308  dtruex  4310  ordsoexmid  4313  nlimsucg  4317  onpsssuc  4322  onintexmid  4324  reg3exmidlemwe  4330  reg3exmid  4331  peano5  4348  limom  4363  0elnn  4367  nn0eln0  4368  nnregexmid  4369  xpeq1  4386  xpeq2  4387  opthprc  4418  xp11m  4786  funopg  4961  dffo4  5342  elunirn  5432  f1oiso  5492  eusvobj2  5525  acexmidlema  5530  acexmidlemb  5531  acexmidlemab  5533  acexmidlem2  5536  mpt2eq123  5591  unielxp  5827  cnvf1o  5873  smoel  5945  tfr0  5967  nnsucelsuc  6100  nntri3or  6102  nntri2  6103  nntri3  6105  nndceq  6107  nnmordi  6119  nnaordex  6130  elqsn0m  6204  qsel  6213  findcard2s  6377  elni2  6469  addnidpig  6491  elinp  6629  pitonn  6981  peano1nnnn  6985  peano2nnnn  6986  peano5nnnn  7023  peano5nni  7992  1nn  8000  peano2nn  8001  dfuzi  8406  uz11  8590  elfzonlteqm1  9167  frec2uzltd  9352  bdsep2  10379  bdzfauscl  10383  bj-indeq  10426  bj-nn0suc0  10448  bj-nnelirr  10451  bj-peano4  10453  bj-inf2vnlem2  10469  bj-nn0sucALT  10476  bj-findis  10477
  Copyright terms: Public domain W3C validator