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

Theorem eleq1 2142
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 2091 . . . 4  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21anbi1d 453 . . 3  |-  ( A  =  B  ->  (
( x  =  A  /\  x  e.  C
)  <->  ( x  =  B  /\  x  e.  C ) ) )
32exbidv 1747 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  A  /\  x  e.  C )  <->  E. x
( x  =  B  /\  x  e.  C
) ) )
4 df-clel 2078 . 2  |-  ( A  e.  C  <->  E. x
( x  =  A  /\  x  e.  C
) )
5 df-clel 2078 . 2  |-  ( B  e.  C  <->  E. x
( x  =  B  /\  x  e.  C
) )
63, 4, 53bitr4g 221 1  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1285   E.wex 1422    e. wcel 1434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  eleq12  2144  eleq1i  2145  eleq1d  2148  eleq1a  2151  cleqh  2179  nelneq  2180  clelsb3  2184  nfcjust  2208  cleqf  2243  nelne2  2337  neleq1  2344  rgen2a  2418  cbvralf  2572  cbvrexf  2573  cbvreu  2576  cbvrab  2600  eqvisset  2610  ceqsralt  2627  vtoclgaf  2664  vtocl2gaf  2666  vtocl3gaf  2668  rspct  2695  rspc  2696  rspce  2697  rspc2gv  2713  ceqsrexv  2726  ceqsrexbv  2727  clel2  2729  elabgt  2736  elabgf  2737  elrabi  2747  elrabf  2748  elrab3t  2749  ralab2  2757  rexab2  2759  mo2icl  2772  morex  2777  reu2  2781  reu6  2782  rmo4  2786  reu8  2789  reuind  2796  nelrdva  2798  ru  2815  dfsbcq  2818  dfsbcq2  2819  sbc8g  2823  sbcel1v  2877  rmob  2907  difjust  2975  unjust  2977  injust  2979  eldif  2983  dfss2f  2991  uniiunlem  3083  elun  3114  elin  3156  rabn0m  3273  disjne  3298  r19.3rm  3331  r19.9rmv  3334  raaanlem  3348  raaan  3349  elpwg  3392  elpr2  3422  elsn2g  3429  rabsn  3461  tpid3g  3507  snssg  3524  difsn  3525  sssnm  3548  opeq1  3572  opeq2  3573  eluni  3606  elunii  3608  eluniab  3615  elint  3644  elintg  3646  elintab  3649  elintrabg  3651  intss1  3653  eliun  3684  eliin  3685  dfiunv2  3716  opabss  3844  cbvmpt  3874  trel  3884  trss  3886  ssex  3917  intnexr  3928  intexabim  3929  iinexgm  3931  euabex  3982  elopab  4015  opelopab2a  4022  frirrg  4107  tz7.2  4111  ordelord  4138  onm  4158  ralxfr2d  4216  rexxfr2d  4217  rabxfrd  4221  reuhypd  4223  ordtriexmid  4267  ordtri2orexmid  4268  ontr2exmid  4270  onsucsssucexmid  4272  onsucelsucexmid  4275  ordsucunielexmid  4276  regexmidlem1  4278  elirr  4286  nordeq  4289  sucprcreg  4294  en2lp  4299  ordsoexmid  4307  ordsuc  4308  onsucuni2  4309  tfis  4326  peano2  4338  findes  4346  limom  4356  opelxp  4394  opeliunxp  4415  opbrop  4439  ssrel  4448  ssrel2  4450  ssrelrel  4460  relopabi  4485  xpiindim  4495  eliunxp  4497  opeliunxp2  4498  ideqg  4509  dmmrnm  4576  dmxpm  4577  elreldm  4582  elrnmptg  4608  elres  4668  resiexg  4677  dfres2  4682  imai  4705  elimasng  4717  issref  4731  xpmlem  4768  xpm  4769  elxp4  4832  elxp5  4833  unielrel  4869  relcnvexb  4881  cnviinm  4883  dmfex  5104  funfveu  5213  funimass4  5250  fvelimab  5255  ssimaex  5260  fvopab3g  5271  fvopab3ig  5272  fvmptssdm  5281  chfnrn  5304  fvelrn  5324  fmpt  5345  ffnfv  5349  fmptco  5356  elunirn  5431  f1elima  5438  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  tfr1onlemaccex  5991  tfrcllemaccex  6004  tfrcl  6007  frecabcl  6042  frecsuc  6050  nntri3or  6130  nntri3  6134  nndcel  6137  iinerm  6237  riinerm  6238  th3qlem1  6267  dom2lem  6311  fiprc  6351  xpsnen  6355  phplem3g  6381  phpelm  6391  ssfiexmid  6401  domfiexmid  6403  snon0  6435  f1dmvrnfibi  6442  f1vrnfibi  6443  ordiso2  6495  elni2  6555  recexnq  6631  recmulnqg  6632  enq0enq  6672  enq0sym  6673  enq0ref  6674  enq0tr  6675  enq0breq  6677  nqnq0pi  6679  nqnq0  6682  prop  6716  prcdnql  6725  prcunqu  6726  prubl  6727  prltlu  6728  prnmaxl  6729  prnminu  6730  prdisj  6733  prarloc  6744  genipv  6750  genpelvl  6753  genpelvu  6754  genprndl  6762  genprndu  6763  distrlem5prl  6827  distrlem5pru  6828  ltexprlemm  6841  ltexprlemdisj  6847  ltexprlemloc  6848  ltexprlemrl  6851  ltexprlemru  6853  aptiprleml  6880  aptiprlemu  6881  archpr  6884  cauappcvgprlemm  6886  cauappcvgprlemladdfu  6895  cauappcvgprlemladdfl  6896  caucvgprlemm  6909  caucvgprlemladdfu  6918  caucvgprprlemmu  6936  elreal2  7050  ltresr  7058  axcnre  7098  0re  7170  renepnf  7217  renemnf  7218  ltxrlt  7234  eqlei2  7261  0cnALT  7354  nn1suc  8114  nnne0  8123  xnn0xr  8412  nn0nepnf  8415  elz  8423  elnn0z  8434  elz2  8489  uzind4s  8748  elnn1uz2  8764  qre  8780  fzsn  9149  fz1sbc  9178  elfzp12  9181  fzm1  9182  fz01or  9193  fvinim0ffz  9316  flqidz  9357  ceilqidz  9387  modqmuladdnn0  9439  frec2uzrand  9476  frecuzrdgtcl  9483  fzfig  9501  iseqfveq2  9533  iseqshft2  9537  monoord  9540  iseqsplit  9543  iseqid2  9553  1exp  9591  bcval  9762  sizeennn  9793  shftlem  9831  shftfibg  9835  shftfib  9838  shftfn  9839  2shfti  9846  rexuz3  10003  sqrt0rlem  10016  cau3  10128  negfi  10237  sumdc  10322  isumrblem  10326  odd2np1  10406  even2n  10407  oddnn02np1  10413  oddge22np1  10414  evennn02n  10415  evennn2n  10416  nn0enne  10435  divalgmod  10460  lcmgcdlem  10592  cncongr1  10618  1nprm  10629  isprm2  10632  dvdsnprmd  10640  exprmfct  10652  nprmdvds1  10654  coprm  10656  elabgf0  10723  bj-rspgt  10732  cbvrald  10734  decidi  10741  sumdc2  10745  bdssex  10836  bj-inex  10841  bj-intnexr  10843  bj-unexg  10855  bj-d0clsepcl  10863  bj-nnelirr  10891  bj-nn0suc  10902  bj-inf2vnlem1  10908  bj-inf2vnlem2  10909  bj-inf2vnlem3  10910  bj-inf2vnlem4  10911  bj-nn0sucALT  10916  bj-findis  10917
  Copyright terms: Public domain W3C validator