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

Theorem eleq2 2084
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 2017 . . . . . 6 (A = Bx(x Ax B))
21biimpi 113 . . . . 5 (A = Bx(x Ax B))
3219.21bi 1434 . . . 4 (A = B → (x Ax B))
43anbi2d 440 . . 3 (A = B → ((x = 𝐶 x A) ↔ (x = 𝐶 x B)))
54exbidv 1689 . 2 (A = B → (x(x = 𝐶 x A) ↔ x(x = 𝐶 x B)))
6 df-clel 2019 . 2 (𝐶 Ax(x = 𝐶 x A))
7 df-clel 2019 . 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 1363   wcel 1375
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 1364  ax-ie2 1365  ax-4 1382  ax-17 1401  ax-ial 1410  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-cleq 2016  df-clel 2019
This theorem is referenced by:  eleq12  2085  eleq2i  2087  eleq2d  2090  nelneq2  2122  clelsb4  2126  dvelimdc  2180  nelne1  2272  neleq2  2279  raleqf  2478  rexeqf  2479  reueq1f  2480  rmoeq1f  2481  rabeqf  2527  clel3g  2654  clel4  2656  sbcel2gv  2798  sbnfc2  2882  difeq2  3032  uneq1  3066  ineq1  3107  n0i  3205  disjel  3250  exsnrex  3386  sneqr  3504  preqr1g  3510  preqr1  3512  preq12b  3514  prel12  3515  elunii  3558  eluniab  3565  ssuni  3575  elinti  3597  elintab  3599  intss1  3603  intmin  3608  intab  3617  iineq2  3647  dfiin2g  3663  breq  3739  axsep2  3849  zfauscl  3850  inuni  3882  rext  3924  intid  3933  mss  3935  opth1  3946  opeqex  3959  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  5720  cnvf1o  5766  smoel  5832  nnsucelsuc  5980  nntri3or  5982  nntri2  5983  nndceq  5985  nnmordi  5995  nnaordex  6006  elqsn0m  6078  qsel  6087  elni2  6167  addnidpig  6188  elinp  6313  bdsep2  6456  bdzfauscl  6460  bj-indeq  6496  peano5set  6509  bj-nn0suc0  6517  bj-nnelirr  6520  bj-peano4  6522
  Copyright terms: Public domain W3C validator