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

Theorem eleq1 2240
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 2187 . . . 4  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21anbi1d 465 . . 3  |-  ( A  =  B  ->  (
( x  =  A  /\  x  e.  C
)  <->  ( x  =  B  /\  x  e.  C ) ) )
32exbidv 1825 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  A  /\  x  e.  C )  <->  E. x
( x  =  B  /\  x  e.  C
) ) )
4 df-clel 2173 . 2  |-  ( A  e.  C  <->  E. x
( x  =  A  /\  x  e.  C
) )
5 df-clel 2173 . 2  |-  ( B  e.  C  <->  E. x
( x  =  B  /\  x  e.  C
) )
63, 4, 53bitr4g 223 1  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    = 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  eleq1i  2243  eleq1d  2246  eleq1a  2249  cleqh  2277  nelneq  2278  clelsb1  2282  nfcjust  2307  cleqf  2344  nelne2  2438  neleq1  2446  rgen2a  2531  cbvralf  2696  cbvrexf  2697  cbvreu  2701  cbvrab  2735  eqvisset  2747  ceqsralt  2764  vtoclgaf  2802  vtocl2gaf  2804  vtocl3gaf  2806  rspct  2834  rspc  2835  rspce  2836  rspc2gv  2853  ceqsrexv  2867  ceqsrexbv  2868  clel2  2870  elabgt  2878  elabgf  2879  elrabi  2890  elrabf  2891  elrab3t  2892  ralab2  2901  rexab2  2903  mo2icl  2916  morex  2921  reu2  2925  reu6  2926  rmo4  2930  reu8  2933  reuind  2942  nelrdva  2944  ru  2961  dfsbcq  2964  dfsbcq2  2965  sbc8g  2970  sbcel1v  3025  rmob  3055  difjust  3130  unjust  3132  injust  3134  eldif  3138  dfss2f  3146  uniiunlem  3244  elun  3276  elin  3318  rabn0m  3450  disjne  3476  r19.3rm  3511  r19.9rmv  3514  raaanlem  3528  raaan  3529  ifmdc  3573  elpwg  3582  elpr2  3613  elsn2g  3624  rabsn  3658  tpid3g  3706  snssb  3724  snssgOLD  3727  difsn  3728  sssnm  3752  opeq1  3776  opeq2  3777  eluni  3810  elunii  3812  eluniab  3819  elint  3848  elintg  3850  elintab  3853  elintrabg  3855  intss1  3857  eliun  3888  eliin  3889  dfiunv2  3920  opabss  4064  cbvmpt  4095  trel  4105  trss  4107  ssex  4137  intnexr  4148  intexabim  4149  exmidel  4202  euabex  4222  elopab  4255  opelopab2a  4262  frirrg  4347  tz7.2  4351  ordelord  4378  onm  4398  ralxfr2d  4461  rexxfr2d  4462  rabxfrd  4466  reuhypd  4468  ordtriexmid  4517  ontriexmidim  4518  ordtri2orexmid  4519  ontr2exmid  4521  onsucsssucexmid  4523  onsucelsucexmid  4526  ordsucunielexmid  4527  regexmidlem1  4529  elirr  4537  nordeq  4540  sucprcreg  4545  en2lp  4550  ordsoexmid  4558  ordsuc  4559  onsucuni2  4560  tfis  4579  peano2  4591  findes  4599  limom  4610  opelxp  4653  opeliunxp  4678  opbrop  4702  ssrel  4711  ssrel2  4713  ssrelrel  4723  relopabi  4749  eliunxp  4762  opeliunxp2  4763  ideqg  4774  dmmrnm  4842  dmxpm  4843  elreldm  4849  elrnmptg  4875  elres  4939  resiexg  4948  dfres2  4955  imai  4980  elimasng  4992  issref  5007  xpmlem  5045  xpm  5046  elxp4  5112  elxp5  5113  unielrel  5152  relcnvexb  5164  dmfex  5401  funfveu  5524  funimass4  5562  fvelimab  5568  ssimaex  5573  fvopab3g  5585  fvopab3ig  5586  fvmptssdm  5596  chfnrn  5623  fvelrn  5643  fmpt  5662  ffnfv  5670  fmptco  5678  elunirn  5761  f1elima  5768  cbvriota  5835  acexmidlemab  5863  acexmidlemcase  5864  cbvmpox  5947  eloprabga  5956  resoprab  5965  elrnmpo  5982  ov  5988  ovig  5990  ov6g  6006  ovg  6007  ovelrn  6017  caovimo  6062  fo1stresm  6156  fo2ndresm  6157  elxp6  6164  unielxp  6169  eqop2  6173  dfoprab4  6187  dfoprab4f  6188  fmpox  6195  1stconst  6216  2ndconst  6217  f1o2ndf1  6223  xporderlem  6226  f1od2  6230  disjxp1  6231  opeliunxp2f  6233  dftpos3  6257  dftpos4  6258  tpostpos  6259  smoel  6295  tfr1onlemaccex  6343  tfrcllemaccex  6356  tfrcl  6359  frecabcl  6394  frecsuc  6402  nntri3or  6488  nntri3  6492  nndcel  6495  riinerm  6602  th3qlem1  6631  mapsncnv  6689  elixpsn  6729  dom2lem  6766  fiprc  6809  xpsnen  6815  phplem3g  6850  phpelm  6860  ssfiexmid  6870  domfiexmid  6872  inffiexmid  6900  undifdcss  6916  snon0  6929  f1dmvrnfibi  6937  f1vrnfibi  6938  ordiso2  7028  ctssdclemn0  7103  ctssdc  7106  enumct  7108  nnnninf  7118  nnnninfeq  7120  nninfisollemne  7123  nninfisol  7125  finomni  7132  exmidlpo  7135  acfun  7200  exmidontriimlem3  7216  exmidontriimlem4  7217  pw1ne1  7222  onntri35  7230  exmidapne  7250  ccfunen  7254  cc2lem  7256  elni2  7304  recexnq  7380  recmulnqg  7381  enq0enq  7421  enq0sym  7422  enq0ref  7423  enq0tr  7424  enq0breq  7426  nqnq0pi  7428  nqnq0  7431  prop  7465  prcdnql  7474  prcunqu  7475  prubl  7476  prltlu  7477  prnmaxl  7478  prnminu  7479  prdisj  7482  prarloc  7493  genipv  7499  genpelvl  7502  genpelvu  7503  genprndl  7511  genprndu  7512  distrlem5prl  7576  distrlem5pru  7577  ltexprlemm  7590  ltexprlemdisj  7596  ltexprlemloc  7597  ltexprlemrl  7600  ltexprlemru  7602  aptiprleml  7629  aptiprlemu  7630  archpr  7633  cauappcvgprlemm  7635  cauappcvgprlemladdfu  7644  cauappcvgprlemladdfl  7645  caucvgprlemm  7658  caucvgprlemladdfu  7667  caucvgprprlemmu  7685  elreal2  7820  ltresr  7829  axcnre  7871  axpre-suploclemres  7891  0re  7948  renepnf  7995  renemnf  7996  ltxrlt  8013  eqlei2  8042  0cnALT  8137  sup3exmid  8903  nn1suc  8927  nnne0  8936  xnn0xr  9233  nn0nepnf  9236  elz  9244  elnn0z  9255  elz2  9313  uzind4s  9579  elnn1uz2  9596  qre  9614  elpqb  9638  xnn0lenn0nn0  9852  xsubge0  9868  xposdif  9869  xleaddadd  9874  fzsn  10052  fz1sbc  10082  elfzp12  10085  fzm1  10086  fz01or  10097  fvinim0ffz  10227  flqidz  10272  ceilqidz  10302  modqmuladdnn0  10354  frec2uzrand  10391  frecuzrdgtcl  10398  fzfig  10416  seq3fveq2  10455  seq3shft2  10459  monoord  10462  seq3split  10465  iseqf1olemqval  10473  seq3id2  10495  1exp  10535  bcval  10713  hashennn  10744  zfz1isolem1  10804  zfz1iso  10805  seq3coll  10806  shftlem  10809  shftfibg  10813  shftfib  10816  shftfn  10817  2shfti  10824  rexuz3  10983  sqrt0rlem  10996  cau3  11108  negfi  11220  sumdc  11350  sumrbdclem  11369  summodclem2a  11373  fisumss  11384  prodrbdclem  11563  prodmodclem2a  11568  fprodssdc  11582  fprodsplit1f  11626  ef0lem  11652  odd2np1  11861  even2n  11862  oddnn02np1  11868  oddge22np1  11869  evennn02n  11870  evennn2n  11871  nn0enne  11890  divalgmod  11915  suprzubdc  11936  zsupssdc  11938  uzwodc  12021  lcmgcdlem  12060  cncongr1  12086  1nprm  12097  isprm2  12100  dvdsnprmd  12108  prmdc  12113  exprmfct  12121  nprmdvds1  12123  coprm  12127  prmdiveq  12219  prm23lt5  12246  pcpre1  12275  pc2dvds  12312  pcz  12314  pcmpt  12324  qexpz  12333  4sqlem2  12370  ennnfonelemhom  12399  ctiunctlemudc  12421  ssnnctlemct  12430  ismgmid  12688  isgrpid2  12803  mhmlem  12867  dvdsrcl2  13093  fiinopn  13169  istopon  13178  basis2  13213  eltg3  13224  tg2  13227  tgidm  13241  bastop  13242  bastop2  13251  topnex  13253  isopn3  13292  tgrest  13336  cnpval  13365  lmbr  13380  cnconst  13401  txbas  13425  uptx  13441  txdis1cn  13445  cnmpt12  13454  cnmpt22  13461  hmeocnvb  13485  xblm  13584  isxms2  13619  mopni  13649  blssioo  13712  dedekindeulemuub  13762  dedekindeulemeu  13767  dedekindicclemuub  13771  dedekindicclemeu  13776  ivthinclemlm  13779  ivthinclemum  13780  lgsfvalg  14073  lgsval2lem  14078  lgsdir2lem2  14097  2sqlem2  14118  2sqlem6  14123  2sqlem7  14124  2sqlem10  14128  elabgf0  14185  bj-rspgt  14194  cbvrald  14196  decidi  14203  sumdc2  14207  bdssex  14310  bj-inex  14315  bj-intnexr  14317  bj-unexg  14329  bj-d0clsepcl  14333  bj-nnelirr  14361  bj-nn0suc  14372  bj-inf2vnlem1  14378  bj-inf2vnlem2  14379  bj-inf2vnlem3  14380  bj-inf2vnlem4  14381  bj-nn0sucALT  14386  bj-findis  14387  trilpolemcl  14441
  Copyright terms: Public domain W3C validator