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

Theorem eleq2 2083
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eleq2 (A = B → (𝐶 A𝐶 B))

Proof of Theorem eleq2
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2016 . . . . . 6 (A = Bx(x Ax B))
21biimpi 113 . . . . 5 (A = Bx(x Ax B))
3219.21bi 1432 . . . 4 (A = B → (x Ax B))
43anbi2d 440 . . 3 (A = B → ((x = 𝐶 x A) ↔ (x = 𝐶 x B)))
54exbidv 1688 . 2 (A = B → (x(x = 𝐶 x A) ↔ x(x = 𝐶 x B)))
6 df-clel 2018 . 2 (𝐶 Ax(x = 𝐶 x A))
7 df-clel 2018 . 2 (𝐶 Bx(x = 𝐶 x B))
85, 6, 73bitr4g 212 1 (A = B → (𝐶 A𝐶 B))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  wal 1226   = wceq 1228  wex 1362   wcel 1374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-clel 2018
This theorem is referenced by:  eleq12  2084  eleq2i  2086  eleq2d  2089  nelneq2  2121  clelsb4  2125  dvelimdc  2179  nelne1  2271  neleq2  2278  raleqf  2477  rexeqf  2478  reueq1f  2479  rmoeq1f  2480  rabeqf  2526  clel3g  2653  clel4  2655  sbcel2gv  2797  sbnfc2  2881  difeq2  3031  uneq1  3065  ineq1  3106  n0i  3204  disjel  3249  exsnrex  3385  sneqr  3503  preqr1g  3509  preqr1  3511  preq12b  3513  prel12  3514  elunii  3557  eluniab  3564  ssuni  3574  elinti  3596  elintab  3598  intss1  3602  intmin  3607  intab  3616  iineq2  3646  dfiin2g  3662  breq  3738  axsep2  3848  zfauscl  3849  inuni  3881  rext  3923  intid  3932  mss  3934  opth1  3945  opeqex  3958  limeq  4061  nsuceq0g  4102  suctrALT  4105  snnex  4129  uniuni  4131  iunpw  4159  ordtriexmidlem  4190  ordtriexmidlem2  4191  ordtriexmid  4192  ordtri2orexmid  4193  onsucelsucexmidlem  4196  onsucelsucexmid  4197  ordsucunielexmid  4198  regexmidlem1  4200  regexmid  4201  elirr  4206  en2lp  4214  suc11g  4217  dtruex  4219  ordsoexmid  4222  nlimsucg  4224  onpsssuc  4229  peano5  4246  limom  4261  0elnn  4265  nn0eln0  4266  nnregexmid  4267  xpeq1  4284  xpeq2  4285  opthprc  4316  xp11m  4684  funopg  4858  dffo4  5238  elunirn  5328  f1oiso  5388  eusvobj2  5420  acexmidlema  5425  acexmidlemb  5426  acexmidlemab  5428  acexmidlem2  5431  mpt2eq123  5485  unielxp  5721  cnvf1o  5767  smoel  5835  nnsucelsuc  5983  nntri3or  5985  nntri2  5986  nndceq  5988  nnmordi  5998  nnaordex  6009  elqsn0m  6083  qsel  6092  elni2  6172  addnidpig  6194  elinp  6326  bdsep2  6791  bdzfauscl  6795  bj-indeq  6831  peano5set  6841  bj-nn0suc0  6851  bj-nnelirr  6854  bj-peano4  6856  bj-inf2vnlem2  6868  bj-nn0sucALT  6875  bj-findis  6876
  Copyright terms: Public domain W3C validator