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

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

Proof of Theorem eleq1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eqeq2 2063 . . . 4  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21anbi1d 446 . . 3  |-  ( A  =  B  ->  (
( x  =  A  /\  x  e.  C
)  <->  ( x  =  B  /\  x  e.  C ) ) )
32exbidv 1720 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  A  /\  x  e.  C )  <->  E. x
( x  =  B  /\  x  e.  C
) ) )
4 df-clel 2050 . 2  |-  ( A  e.  C  <->  E. x
( x  =  A  /\  x  e.  C
) )
5 df-clel 2050 . 2  |-  ( B  e.  C  <->  E. x
( x  =  B  /\  x  e.  C
) )
63, 4, 53bitr4g 216 1  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102    = wceq 1257   E.wex 1395    e. wcel 1407
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-4 1414  ax-17 1433  ax-ial 1441  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-cleq 2047  df-clel 2050
This theorem is referenced by:  eleq12  2116  eleq1i  2117  eleq1d  2120  eleq1a  2123  cleqh  2151  nelneq  2152  clelsb3  2156  nfcjust  2180  cleqf  2215  nelne2  2309  neleq1  2316  rgen2a  2390  cbvralf  2542  cbvrexf  2543  cbvreu  2546  cbvrab  2570  eqvisset  2580  ceqsralt  2596  vtoclgaf  2633  vtocl2gaf  2635  vtocl3gaf  2637  rspct  2664  rspc  2665  rspce  2666  ceqsrexv  2694  ceqsrexbv  2695  clel2  2697  elabgt  2704  elabgf  2705  elrabi  2715  elrabf  2716  elrab3t  2717  ralab2  2725  rexab2  2727  mo2icl  2740  morex  2745  reu2  2749  reu6  2750  rmo4  2754  reu8  2757  reuind  2764  nelrdva  2766  ru  2783  dfsbcq  2786  dfsbcq2  2787  sbc8g  2791  sbcel1v  2845  rmob  2875  difjust  2944  unjust  2946  injust  2948  eldif  2952  dfss2f  2961  uniiunlem  3053  elun  3109  elin  3151  rabn0m  3270  disjne  3298  r19.3rm  3335  r19.9rmv  3338  raaanlem  3351  raaan  3352  elpwg  3392  elpr2  3422  elsn2g  3429  rabsn  3462  tpid3g  3508  snssg  3525  difsn  3526  sssnm  3550  opeq1  3574  opeq2  3575  eluni  3608  elunii  3610  eluniab  3617  elint  3646  elintg  3648  elintab  3651  elintrabg  3653  intss1  3655  eliun  3686  eliin  3687  dfiunv2  3718  opabss  3846  cbvmpt  3876  trel  3886  trss  3888  ssex  3919  intnexr  3930  intexabim  3931  iinexgm  3933  euabex  3986  elopab  4020  opelopab2a  4027  frirrg  4112  tz7.2  4116  ordelord  4143  onm  4163  ralxfr2d  4221  rexxfr2d  4222  rabxfrd  4226  reuhypd  4228  ordtriexmid  4272  ordtri2orexmid  4273  ontr2exmid  4275  onsucsssucexmid  4277  onsucelsucexmid  4280  ordsucunielexmid  4281  regexmidlem1  4283  elirr  4291  nordeq  4293  sucprcreg  4298  en2lp  4303  ordsoexmid  4311  ordsuc  4312  onsucuni2  4313  tfis  4331  peano2  4343  findes  4351  limom  4361  opelxp  4399  opeliunxp  4420  opbrop  4444  ssrel  4453  ssrel2  4455  ssrelrel  4465  relopabi  4488  xpiindim  4498  eliunxp  4500  opeliunxp2  4501  ideqg  4512  dmmrnm  4579  dmxpm  4580  elreldm  4585  elrnmptg  4611  elres  4671  resiexg  4678  dfres2  4683  imai  4706  elimasng  4718  issref  4732  xpmlem  4769  xpm  4770  elxp4  4833  elxp5  4834  unielrel  4870  relcnvexb  4882  cnviinm  4884  dmfex  5104  funfveu  5213  funimass4  5249  fvelimab  5254  ssimaex  5259  fvopab3g  5270  fvopab3ig  5271  fvmptssdm  5280  chfnrn  5303  fvelrn  5323  fmpt  5344  ffnfv  5348  fmptco  5355  elunirn  5430  f1elima  5437  cbvriota  5503  acexmidlemab  5531  acexmidlemcase  5532  cbvmpt2x  5607  eloprabga  5616  resoprab  5622  elrnmpt2  5639  ov  5645  ovig  5647  ov6g  5663  ovg  5664  ovelrn  5674  caovimo  5719  fo1stresm  5813  fo2ndresm  5814  elxp6  5821  unielxp  5825  eqop2  5829  dfoprab4  5843  dfoprab4f  5844  fmpt2x  5851  1stconst  5867  2ndconst  5868  f1o2ndf1  5874  xporderlem  5877  f1od2  5881  dftpos3  5905  dftpos4  5906  tpostpos  5907  smoel  5943  frecsuc  6019  freccl  6021  nntri3or  6100  nntri3  6103  nndcel  6106  iinerm  6206  riinerm  6207  th3qlem1  6236  dom2lem  6280  fiprc  6320  xpsnen  6323  phplem3g  6347  phpelm  6356  ssfiexmid  6364  snon0  6384  ordiso2  6385  elni2  6440  recexnq  6516  recmulnqg  6517  enq0enq  6557  enq0sym  6558  enq0ref  6559  enq0tr  6560  enq0breq  6562  nqnq0pi  6564  nqnq0  6567  prop  6601  prcdnql  6610  prcunqu  6611  prubl  6612  prltlu  6613  prnmaxl  6614  prnminu  6615  prdisj  6618  prarloc  6629  genipv  6635  genpelvl  6638  genpelvu  6639  genprndl  6647  genprndu  6648  distrlem5prl  6712  distrlem5pru  6713  ltexprlemm  6726  ltexprlemdisj  6732  ltexprlemloc  6733  ltexprlemrl  6736  ltexprlemru  6738  aptiprleml  6765  aptiprlemu  6766  archpr  6769  cauappcvgprlemm  6771  cauappcvgprlemladdfu  6780  cauappcvgprlemladdfl  6781  caucvgprlemm  6794  caucvgprlemladdfu  6803  caucvgprprlemmu  6821  elreal2  6935  ltresr  6943  axcnre  6983  0re  7055  renepnf  7102  renemnf  7103  ltxrlt  7114  eqlei2  7141  0cnALT  7234  nn1suc  7979  nnne0  7988  elz  8274  elnn0z  8285  elz2  8340  uzind4s  8599  elnn1uz2  8611  qre  8627  fzsn  9001  fz1sbc  9030  elfzp12  9033  fzm1  9034  fvinim0ffz  9168  flqidz  9201  ceilqidz  9231  modqmuladdnn0  9283  frec2uzrand  9320  frecuzrdgfn  9327  fzfig  9335  iseqfveq2  9357  iseqshft2  9361  monoord  9364  iseqsplit  9367  1exp  9414  bcval  9581  shftlem  9609  shftfibg  9613  shftfib  9616  shftfn  9617  2shfti  9624  rexuz3  9780  sqrt0rlem  9793  cau3  9905  odd2np1  10147  even2n  10148  fz01or  10153  oddnn02np1  10155  oddge22np1  10156  evennn02n  10157  evennn2n  10158  nn0enne  10177  elabgf0  10246  bj-rspgt  10255  cbvrald  10257  bdssex  10352  bj-inex  10357  bj-intnexr  10359  bj-unexg  10371  bj-d0clsepcl  10379  bj-nnelirr  10408  bj-nn0suc  10419  bj-inf2vnlem1  10425  bj-inf2vnlem2  10426  bj-inf2vnlem3  10427  bj-inf2vnlem4  10428  bj-nn0sucALT  10433  bj-findis  10434
  Copyright terms: Public domain W3C validator