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

Theorem eleq2 2077
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 2010 . . . . . 6 (A = Bx(x Ax B))
21biimpi 113 . . . . 5 (A = Bx(x Ax B))
3219.21bi 1426 . . . 4 (A = B → (x Ax B))
43anbi2d 437 . . 3 (A = B → ((x = 𝐶 x A) ↔ (x = 𝐶 x B)))
54exbidv 1682 . 2 (A = B → (x(x = 𝐶 x A) ↔ x(x = 𝐶 x B)))
6 df-clel 2012 . 2 (𝐶 Ax(x = 𝐶 x A))
7 df-clel 2012 . 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 1224   = wceq 1226  wex 1357   wcel 1369
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 1312  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-4 1376  ax-17 1395  ax-ial 1403  ax-ext 1998
This theorem depends on definitions:  df-bi 110  df-cleq 2009  df-clel 2012
This theorem is referenced by:  eleq12  2078  eleq2i  2080  eleq2d  2083  nelneq2  2115  clelsb4  2119  dvelimdc  2173  nelne1  2267  neleq2  2274  raleqf  2473  rexeqf  2474  reueq1f  2475  rmoeq1f  2476  rabeqf  2522  clel3g  2649  clel4  2651  sbcel2gv  2793  sbnfc2  2877  difeq2  3027  uneq1  3061  ineq1  3102  n0i  3200  disjel  3245  exsnrex  3379  sneqr  3497  preqr1g  3503  preqr1  3505  preq12b  3507  prel12  3508  elunii  3551  eluniab  3558  ssuni  3568  elinti  3590  elintab  3592  intss1  3596  intmin  3601  intab  3610  iineq2  3640  dfiin2g  3656  breq  3732  axsep2  3842  zfauscl  3843  inuni  3875  rext  3917  intid  3926  mss  3928  opth1  3939  opeqex  3952  limeq  4055  nsuceq0g  4096  suctr  4099  snnex  4122  uniuni  4124  iunpw  4152  ordtriexmidlem  4183  ordtriexmidlem2  4184  ordtriexmid  4185  ordtri2orexmid  4186  onsucelsucexmidlem  4189  onsucelsucexmid  4190  ordsucunielexmid  4191  regexmidlem1  4193  regexmid  4194  elirr  4199  en2lp  4207  suc11g  4210  dtruex  4212  ordsoexmid  4215  nlimsucg  4217  onpsssuc  4222  peano5  4239  limom  4254  0elnn  4258  nn0eln0  4259  nnregexmid  4260  xpeq1  4277  xpeq2  4278  opthprc  4309  xp11m  4677  funopg  4851  dffo4  5231  elunirn  5321  f1oiso  5381  eusvobj2  5413  acexmidlema  5418  acexmidlemb  5419  acexmidlemab  5421  acexmidlem2  5424  mpt2eq123  5478  unielxp  5714  cnvf1o  5760  smoel  5828  nnsucelsuc  5976  nntri3or  5978  nntri2  5979  nndceq  5981  nnmordi  5991  nnaordex  6002  elqsn0m  6076  qsel  6085  elni2  6163  addnidpig  6185  elinp  6317  peano5nni  7503  1nn  7511  peano2nn  7512  dfuzi  7916  bdsep2  8462  bdzfauscl  8466  bj-indeq  8506  peano5set  8516  bj-nn0suc0  8526  bj-nnelirr  8529  bj-peano4  8531  bj-inf2vnlem2  8543  bj-nn0sucALT  8550  bj-findis  8551
  Copyright terms: Public domain W3C validator