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

Theorem eleq2 2241
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eleq2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2171 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 120 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1558 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 464 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1825 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2173 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2173 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 223 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105   A.wal 1351    = wceq 1353   E.wex 1492    e. wcel 2148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173
This theorem is referenced by:  eleq12  2242  eleq2i  2244  eleq2d  2247  nelneq2  2279  clelsb2  2283  dvelimdc  2340  nelne1  2437  neleq2  2447  raleqf  2668  rexeqf  2669  reueq1f  2670  rmoeq1f  2671  rabeqf  2727  clel3g  2871  clel4  2873  sbcbi2  3013  sbcel2gv  3026  csbeq2  3081  sbnfc2  3117  difeq2  3247  uneq1  3282  ineq1  3329  nel02  3427  n0i  3428  disjel  3477  exsnrex  3633  sneqr  3758  preqr1g  3764  preqr1  3766  preq12b  3768  prel12  3769  elunii  3812  eluniab  3819  ssuni  3829  elinti  3851  elintab  3853  intss1  3857  intmin  3862  intab  3871  iineq2  3901  dfiin2g  3917  breq  4002  axsep2  4119  zfauscl  4120  inuni  4152  exmidexmid  4193  ss1o0el1  4194  exmid01  4195  exmidundif  4203  exmidundifim  4204  rext  4211  intid  4220  mss  4222  opth1  4232  opeqex  4245  frforeq3  4343  frirrg  4346  limeq  4373  nsuceq0g  4414  suctr  4417  snnex  4444  uniuni  4447  iunpw  4476  ordtriexmidlem  4514  ordtriexmidlem2  4515  ordtriexmid  4516  ontriexmidim  4517  ordtri2orexmid  4518  ontr2exmid  4520  ordtri2or2exmidlem  4521  onsucelsucexmidlem  4524  onsucelsucexmid  4525  ordsucunielexmid  4526  regexmidlem1  4528  reg2exmidlema  4529  regexmid  4530  reg2exmid  4531  elirr  4536  en2lp  4549  suc11g  4552  dtruex  4554  ordsoexmid  4557  nlimsucg  4561  onintexmid  4568  reg3exmidlemwe  4574  reg3exmid  4575  peano5  4593  limom  4609  0elnn  4614  nn0eln0  4615  nnregexmid  4616  xpeq1  4636  xpeq2  4637  opthprc  4673  xp11m  5062  funopg  5245  dffo4  5659  elunirn  5760  f1oiso  5820  canth  5822  eusvobj2  5854  acexmidlema  5859  acexmidlemb  5860  acexmidlemab  5862  acexmidlem2  5865  mpoeq123  5927  oprssdmm  6165  unielxp  6168  cnvf1o  6219  smoel  6294  tfr0dm  6316  frecabcl  6393  nnsucelsuc  6485  nntri3or  6487  nntri2  6488  nntri3  6491  nndceq  6493  nnmordi  6510  nnaordex  6522  elqsn0m  6596  qsel  6605  mapsn  6683  findcard2s  6883  undifdcss  6915  ctssdclemr  7104  nnnninf2  7118  exmidonfinlem  7185  exmidfodomrlemr  7194  exmidfodomrlemrALT  7195  exmidaclem  7200  exmidontriimlem3  7215  exmidontriimlem4  7216  exmidontriim  7217  pw1ne3  7222  sucpw1ne3  7224  sucpw1nel3  7225  onntri35  7229  elni2  7291  addnidpig  7313  elinp  7451  suplocexprlemdisj  7697  suplocexprlemub  7700  pitonn  7825  peano1nnnn  7829  peano2nnnn  7830  peano5nnnn  7869  sup3exmid  8890  peano5nni  8898  1nn  8906  peano2nn  8907  dfuzi  9339  uz11  9526  elfzonlteqm1  10183  frec2uzltd  10376  0tonninf  10412  1tonninf  10413  sumeq1  11334  prodeq1f  11531  ctiunct  12411  ssomct  12416  issubm  12740  istopg  13130  fiinbas  13180  topbas  13200  epttop  13223  restbasg  13301  icnpimaex  13344  lmcvg  13350  iscnp4  13351  cncnpi  13361  cnconst2  13366  cnptoprest  13372  cnptoprest2  13373  cnpdis  13375  lmss  13379  lmff  13382  txbas  13391  eltx  13392  txcnp  13404  txlm  13412  blssps  13560  blss  13561  blssexps  13562  blssex  13563  neibl  13624  metss  13627  metrest  13639  xmettx  13643  metcnp3  13644  tgioo  13679  tgqioo  13680  bdsep2  14260  bdzfauscl  14264  bj-indeq  14303  bj-nn0suc0  14324  bj-nnelirr  14327  bj-peano4  14329  bj-inf2vnlem2  14345  bj-nn0sucALT  14352  bj-findis  14353  strcollnft  14358  sscoll2  14362  nninfsellemdc  14382  nninfsellemqall  14387
  Copyright terms: Public domain W3C validator