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

Theorem eleq2 2204
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 2134 . . . . . 6 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 119 . . . . 5 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1538 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
43anbi2d 460 . . 3 (𝐴 = 𝐵 → ((𝑥 = 𝐶𝑥𝐴) ↔ (𝑥 = 𝐶𝑥𝐵)))
54exbidv 1798 . 2 (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2136 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2136 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73bitr4g 222 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1330   = wceq 1332  wex 1469  wcel 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136
This theorem is referenced by:  eleq12  2205  eleq2i  2207  eleq2d  2210  nelneq2  2242  clelsb4  2246  dvelimdc  2302  nelne1  2399  neleq2  2409  raleqf  2625  rexeqf  2626  reueq1f  2627  rmoeq1f  2628  rabeqf  2679  clel3g  2822  clel4  2824  sbcbi2  2962  sbcel2gv  2975  csbeq2  3030  sbnfc2  3064  difeq2  3192  uneq1  3227  ineq1  3274  n0i  3372  disjel  3421  exsnrex  3572  sneqr  3694  preqr1g  3700  preqr1  3702  preq12b  3704  prel12  3705  elunii  3748  eluniab  3755  ssuni  3765  elinti  3787  elintab  3789  intss1  3793  intmin  3798  intab  3807  iineq2  3837  dfiin2g  3853  breq  3938  axsep2  4054  zfauscl  4055  inuni  4087  exmidexmid  4127  exmid01  4128  exmidundif  4136  exmidundifim  4137  rext  4144  intid  4153  mss  4155  opth1  4165  opeqex  4178  frforeq3  4276  frirrg  4279  limeq  4306  nsuceq0g  4347  suctr  4350  snnex  4376  uniuni  4379  iunpw  4408  ordtriexmidlem  4442  ordtriexmidlem2  4443  ordtriexmid  4444  ordtri2orexmid  4445  ontr2exmid  4447  ordtri2or2exmidlem  4448  onsucelsucexmidlem  4451  onsucelsucexmid  4452  ordsucunielexmid  4453  regexmidlem1  4455  reg2exmidlema  4456  regexmid  4457  reg2exmid  4458  elirr  4463  en2lp  4476  suc11g  4479  dtruex  4481  ordsoexmid  4484  nlimsucg  4488  onintexmid  4494  reg3exmidlemwe  4500  reg3exmid  4501  peano5  4519  limom  4534  0elnn  4539  nn0eln0  4540  nnregexmid  4541  xpeq1  4560  xpeq2  4561  opthprc  4597  xp11m  4984  funopg  5164  dffo4  5575  elunirn  5674  f1oiso  5734  eusvobj2  5767  acexmidlema  5772  acexmidlemb  5773  acexmidlemab  5775  acexmidlem2  5778  mpoeq123  5837  oprssdmm  6076  unielxp  6079  cnvf1o  6129  smoel  6204  tfr0dm  6226  frecabcl  6303  nnsucelsuc  6394  nntri3or  6396  nntri2  6397  nntri3  6400  nndceq  6402  nnmordi  6419  nnaordex  6430  elqsn0m  6504  qsel  6513  mapsn  6591  findcard2s  6791  undifdcss  6818  ctssdclemr  7004  exmidonfinlem  7065  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  exmidaclem  7080  elni2  7145  addnidpig  7167  elinp  7305  suplocexprlemdisj  7551  suplocexprlemub  7554  pitonn  7679  peano1nnnn  7683  peano2nnnn  7684  peano5nnnn  7723  sup3exmid  8738  peano5nni  8746  1nn  8754  peano2nn  8755  dfuzi  9184  uz11  9371  elfzonlteqm1  10017  frec2uzltd  10206  0tonninf  10242  1tonninf  10243  sumeq1  11155  prodeq1f  11352  ctiunct  11987  istopg  12203  fiinbas  12253  topbas  12273  epttop  12296  restbasg  12374  icnpimaex  12417  lmcvg  12423  iscnp4  12424  cncnpi  12434  cnconst2  12439  cnptoprest  12445  cnptoprest2  12446  cnpdis  12448  lmss  12452  lmff  12455  txbas  12464  eltx  12465  txcnp  12477  txlm  12485  blssps  12633  blss  12634  blssexps  12635  blssex  12636  neibl  12697  metss  12700  metrest  12712  xmettx  12716  metcnp3  12717  tgioo  12752  tgqioo  12753  bdsep2  13253  bdzfauscl  13257  bj-indeq  13296  bj-nn0suc0  13317  bj-nnelirr  13320  bj-peano4  13322  bj-inf2vnlem2  13338  bj-nn0sucALT  13345  bj-findis  13346  strcollnft  13351  sscoll2  13355  nninfsellemdc  13379  nninfsellemqall  13384
  Copyright terms: Public domain W3C validator