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

Theorem eleq1 2240
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eleq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem eleq1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 eqeq2 2187 . . . 4 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21anbi1d 465 . . 3 (𝐴 = 𝐵 → ((𝑥 = 𝐴𝑥𝐶) ↔ (𝑥 = 𝐵𝑥𝐶)))
32exbidv 1825 . 2 (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴𝑥𝐶) ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐶)))
4 df-clel 2173 . 2 (𝐴𝐶 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐶))
5 df-clel 2173 . 2 (𝐵𝐶 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐶))
63, 4, 53bitr4g 223 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wex 1492  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  ccfunen  7251  cc2lem  7253  elni2  7301  recexnq  7377  recmulnqg  7378  enq0enq  7418  enq0sym  7419  enq0ref  7420  enq0tr  7421  enq0breq  7423  nqnq0pi  7425  nqnq0  7428  prop  7462  prcdnql  7471  prcunqu  7472  prubl  7473  prltlu  7474  prnmaxl  7475  prnminu  7476  prdisj  7479  prarloc  7490  genipv  7496  genpelvl  7499  genpelvu  7500  genprndl  7508  genprndu  7509  distrlem5prl  7573  distrlem5pru  7574  ltexprlemm  7587  ltexprlemdisj  7593  ltexprlemloc  7594  ltexprlemrl  7597  ltexprlemru  7599  aptiprleml  7626  aptiprlemu  7627  archpr  7630  cauappcvgprlemm  7632  cauappcvgprlemladdfu  7641  cauappcvgprlemladdfl  7642  caucvgprlemm  7655  caucvgprlemladdfu  7664  caucvgprprlemmu  7682  elreal2  7817  ltresr  7826  axcnre  7868  axpre-suploclemres  7888  0re  7945  renepnf  7992  renemnf  7993  ltxrlt  8010  eqlei2  8039  0cnALT  8134  sup3exmid  8900  nn1suc  8924  nnne0  8933  xnn0xr  9230  nn0nepnf  9233  elz  9241  elnn0z  9252  elz2  9310  uzind4s  9576  elnn1uz2  9593  qre  9611  elpqb  9635  xnn0lenn0nn0  9849  xsubge0  9865  xposdif  9866  xleaddadd  9871  fzsn  10049  fz1sbc  10079  elfzp12  10082  fzm1  10083  fz01or  10094  fvinim0ffz  10224  flqidz  10269  ceilqidz  10299  modqmuladdnn0  10351  frec2uzrand  10388  frecuzrdgtcl  10395  fzfig  10413  seq3fveq2  10452  seq3shft2  10456  monoord  10459  seq3split  10462  iseqf1olemqval  10470  seq3id2  10492  1exp  10532  bcval  10710  hashennn  10741  zfz1isolem1  10801  zfz1iso  10802  seq3coll  10803  shftlem  10806  shftfibg  10810  shftfib  10813  shftfn  10814  2shfti  10821  rexuz3  10980  sqrt0rlem  10993  cau3  11105  negfi  11217  sumdc  11347  sumrbdclem  11366  summodclem2a  11370  fisumss  11381  prodrbdclem  11560  prodmodclem2a  11565  fprodssdc  11579  fprodsplit1f  11623  ef0lem  11649  odd2np1  11858  even2n  11859  oddnn02np1  11865  oddge22np1  11866  evennn02n  11867  evennn2n  11868  nn0enne  11887  divalgmod  11912  suprzubdc  11933  zsupssdc  11935  uzwodc  12018  lcmgcdlem  12057  cncongr1  12083  1nprm  12094  isprm2  12097  dvdsnprmd  12105  prmdc  12110  exprmfct  12118  nprmdvds1  12120  coprm  12124  prmdiveq  12216  prm23lt5  12243  pcpre1  12272  pc2dvds  12309  pcz  12311  pcmpt  12321  qexpz  12330  4sqlem2  12367  ennnfonelemhom  12396  ctiunctlemudc  12418  ssnnctlemct  12427  ismgmid  12685  isgrpid2  12800  mhmlem  12864  dvdsrcl2  13090  fiinopn  13162  istopon  13171  basis2  13206  eltg3  13217  tg2  13220  tgidm  13234  bastop  13235  bastop2  13244  topnex  13246  isopn3  13285  tgrest  13329  cnpval  13358  lmbr  13373  cnconst  13394  txbas  13418  uptx  13434  txdis1cn  13438  cnmpt12  13447  cnmpt22  13454  hmeocnvb  13478  xblm  13577  isxms2  13612  mopni  13642  blssioo  13705  dedekindeulemuub  13755  dedekindeulemeu  13760  dedekindicclemuub  13764  dedekindicclemeu  13769  ivthinclemlm  13772  ivthinclemum  13773  lgsfvalg  14066  lgsval2lem  14071  lgsdir2lem2  14090  2sqlem2  14111  2sqlem6  14116  2sqlem7  14117  2sqlem10  14121  elabgf0  14178  bj-rspgt  14187  cbvrald  14189  decidi  14196  sumdc2  14200  bdssex  14303  bj-inex  14308  bj-intnexr  14310  bj-unexg  14322  bj-d0clsepcl  14326  bj-nnelirr  14354  bj-nn0suc  14365  bj-inf2vnlem1  14371  bj-inf2vnlem2  14372  bj-inf2vnlem3  14373  bj-inf2vnlem4  14374  bj-nn0sucALT  14379  bj-findis  14380  trilpolemcl  14434
  Copyright terms: Public domain W3C validator