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

Theorem eleq2 2146
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 2077 . . . . . 6 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 118 . . . . 5 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1491 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
43anbi2d 452 . . 3 (𝐴 = 𝐵 → ((𝑥 = 𝐶𝑥𝐴) ↔ (𝑥 = 𝐶𝑥𝐵)))
54exbidv 1748 . 2 (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐶𝑥𝐴) ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵)))
6 df-clel 2079 . 2 (𝐶𝐴 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐴))
7 df-clel 2079 . 2 (𝐶𝐵 ↔ ∃𝑥(𝑥 = 𝐶𝑥𝐵))
85, 6, 73bitr4g 221 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wal 1283   = wceq 1285  wex 1422  wcel 1434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-clel 2079
This theorem is referenced by:  eleq12  2147  eleq2i  2149  eleq2d  2152  nelneq2  2184  clelsb4  2188  dvelimdc  2242  nelne1  2339  neleq2  2349  raleqf  2551  rexeqf  2552  reueq1f  2553  rmoeq1f  2554  rabeqf  2602  clel3g  2739  clel4  2741  sbcbi2  2875  sbcel2gv  2888  sbnfc2  2973  difeq2  3096  uneq1  3131  ineq1  3178  n0i  3274  disjel  3319  exsnrex  3459  sneqr  3578  preqr1g  3584  preqr1  3586  preq12b  3588  prel12  3589  elunii  3632  eluniab  3639  ssuni  3649  elinti  3671  elintab  3673  intss1  3677  intmin  3682  intab  3691  iineq2  3721  dfiin2g  3737  breq  3813  axsep2  3923  zfauscl  3924  inuni  3956  exmidexmid  3994  exmid01  3995  exmidundif  3998  rext  4005  intid  4014  mss  4016  opth1  4026  opeqex  4039  frforeq3  4137  frirrg  4140  limeq  4167  nsuceq0g  4208  suctr  4211  snnex  4234  uniuni  4236  iunpw  4264  ordtriexmidlem  4298  ordtriexmidlem2  4299  ordtriexmid  4300  ordtri2orexmid  4301  ontr2exmid  4303  ordtri2or2exmidlem  4304  onsucelsucexmidlem  4307  onsucelsucexmid  4308  ordsucunielexmid  4309  regexmidlem1  4311  reg2exmidlema  4312  regexmid  4313  reg2exmid  4314  elirr  4319  en2lp  4332  suc11g  4335  dtruex  4337  ordsoexmid  4340  nlimsucg  4344  onintexmid  4350  reg3exmidlemwe  4356  reg3exmid  4357  peano5  4375  limom  4390  0elnn  4394  nn0eln0  4395  nnregexmid  4396  xpeq1  4414  xpeq2  4415  opthprc  4446  xp11m  4822  funopg  5000  dffo4  5391  elunirn  5484  f1oiso  5543  eusvobj2  5576  acexmidlema  5581  acexmidlemb  5582  acexmidlemab  5584  acexmidlem2  5587  mpt2eq123  5642  unielxp  5878  cnvf1o  5924  smoel  5996  tfr0dm  6018  frecabcl  6095  nnsucelsuc  6183  nntri3or  6185  nntri2  6186  nntri3  6189  nndceq  6191  nnmordi  6204  nnaordex  6215  elqsn0m  6289  qsel  6298  mapsn  6376  findcard2s  6535  undifdcss  6559  exmidfodomrlemr  6730  exmidfodomrlemrALT  6731  elni2  6775  addnidpig  6797  elinp  6935  pitonn  7287  peano1nnnn  7291  peano2nnnn  7292  peano5nnnn  7329  peano5nni  8318  1nn  8326  peano2nn  8327  dfuzi  8751  uz11  8935  elfzonlteqm1  9509  frec2uzltd  9698  0tonninf  9733  1tonninf  9734  sumeq1  10565  bdsep2  11119  bdzfauscl  11123  bj-indeq  11166  bj-nn0suc0  11187  bj-nnelirr  11190  bj-peano4  11192  bj-inf2vnlem2  11208  bj-nn0sucALT  11215  bj-findis  11216
  Copyright terms: Public domain W3C validator