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

Theorem eleq1 2147
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 2094 . . . 4 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21anbi1d 453 . . 3 (𝐴 = 𝐵 → ((𝑥 = 𝐴𝑥𝐶) ↔ (𝑥 = 𝐵𝑥𝐶)))
32exbidv 1750 . 2 (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴𝑥𝐶) ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐶)))
4 df-clel 2081 . 2 (𝐴𝐶 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐶))
5 df-clel 2081 . 2 (𝐵𝐶 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐶))
63, 4, 53bitr4g 221 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1287  wex 1424  wcel 1436
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  eleq12  2149  eleq1i  2150  eleq1d  2153  eleq1a  2156  cleqh  2184  nelneq  2185  clelsb3  2189  nfcjust  2213  cleqf  2248  nelne2  2342  neleq1  2350  rgen2a  2425  cbvralf  2580  cbvrexf  2581  cbvreu  2584  cbvrab  2613  eqvisset  2623  ceqsralt  2640  vtoclgaf  2677  vtocl2gaf  2679  vtocl3gaf  2681  rspct  2708  rspc  2709  rspce  2710  rspc2gv  2725  ceqsrexv  2738  ceqsrexbv  2739  clel2  2741  elabgt  2748  elabgf  2749  elrabi  2759  elrabf  2760  elrab3t  2761  ralab2  2770  rexab2  2772  mo2icl  2785  morex  2790  reu2  2794  reu6  2795  rmo4  2799  reu8  2802  reuind  2809  nelrdva  2811  ru  2828  dfsbcq  2831  dfsbcq2  2832  sbc8g  2836  sbcel1v  2890  rmob  2920  difjust  2989  unjust  2991  injust  2993  eldif  2997  dfss2f  3005  uniiunlem  3098  elun  3130  elin  3172  rabn0m  3299  disjne  3324  r19.3rm  3357  r19.9rmv  3360  raaanlem  3374  raaan  3375  ifmdc  3414  elpwg  3423  elpr2  3453  elsn2g  3462  rabsn  3494  tpid3g  3540  snssg  3558  difsn  3559  sssnm  3583  opeq1  3607  opeq2  3608  eluni  3641  elunii  3643  eluniab  3650  elint  3679  elintg  3681  elintab  3684  elintrabg  3686  intss1  3688  eliun  3719  eliin  3720  dfiunv2  3751  opabss  3879  cbvmpt  3910  trel  3920  trss  3922  ssex  3953  intnexr  3964  intexabim  3965  iinexgm  3967  exmidel  4010  euabex  4028  elopab  4061  opelopab2a  4068  frirrg  4153  tz7.2  4157  ordelord  4184  onm  4204  ralxfr2d  4262  rexxfr2d  4263  rabxfrd  4267  reuhypd  4269  ordtriexmid  4313  ordtri2orexmid  4314  ontr2exmid  4316  onsucsssucexmid  4318  onsucelsucexmid  4321  ordsucunielexmid  4322  regexmidlem1  4324  elirr  4332  nordeq  4335  sucprcreg  4340  en2lp  4345  ordsoexmid  4353  ordsuc  4354  onsucuni2  4355  tfis  4373  peano2  4385  findes  4393  limom  4403  opelxp  4442  opeliunxp  4463  opbrop  4487  ssrel  4496  ssrel2  4498  ssrelrel  4508  relopabi  4533  xpiindim  4543  eliunxp  4545  opeliunxp2  4546  ideqg  4557  dmmrnm  4625  dmxpm  4626  elreldm  4631  elrnmptg  4657  elres  4717  resiexg  4726  dfres2  4733  imai  4757  elimasng  4769  issref  4783  xpmlem  4820  xpm  4821  elxp4  4886  elxp5  4887  unielrel  4926  relcnvexb  4938  cnviinm  4940  dmfex  5165  funfveu  5283  funimass4  5320  fvelimab  5325  ssimaex  5330  fvopab3g  5342  fvopab3ig  5343  fvmptssdm  5352  chfnrn  5375  fvelrn  5395  fmpt  5414  ffnfv  5421  fmptco  5429  elunirn  5508  f1elima  5515  cbvriota  5581  acexmidlemab  5609  acexmidlemcase  5610  cbvmpt2x  5685  eloprabga  5694  resoprab  5700  elrnmpt2  5717  ov  5723  ovig  5725  ov6g  5741  ovg  5742  ovelrn  5752  caovimo  5797  fo1stresm  5891  fo2ndresm  5892  elxp6  5899  unielxp  5903  eqop2  5907  dfoprab4  5921  dfoprab4f  5922  fmpt2x  5929  1stconst  5945  2ndconst  5946  f1o2ndf1  5952  xporderlem  5955  f1od2  5959  dftpos3  5983  dftpos4  5984  tpostpos  5985  smoel  6021  tfr1onlemaccex  6069  tfrcllemaccex  6082  tfrcl  6085  frecabcl  6120  frecsuc  6128  nntri3or  6210  nntri3  6214  nndcel  6217  iinerm  6318  riinerm  6319  th3qlem1  6348  mapsncnv  6406  dom2lem  6443  fiprc  6486  xpsnen  6491  phplem3g  6526  phpelm  6536  ssfiexmid  6546  domfiexmid  6548  inffiexmid  6576  undifdcss  6587  snon0  6598  f1dmvrnfibi  6606  f1vrnfibi  6607  ordiso2  6675  djuun  6707  finomni  6743  nnnninf  6753  elni2  6820  recexnq  6896  recmulnqg  6897  enq0enq  6937  enq0sym  6938  enq0ref  6939  enq0tr  6940  enq0breq  6942  nqnq0pi  6944  nqnq0  6947  prop  6981  prcdnql  6990  prcunqu  6991  prubl  6992  prltlu  6993  prnmaxl  6994  prnminu  6995  prdisj  6998  prarloc  7009  genipv  7015  genpelvl  7018  genpelvu  7019  genprndl  7027  genprndu  7028  distrlem5prl  7092  distrlem5pru  7093  ltexprlemm  7106  ltexprlemdisj  7112  ltexprlemloc  7113  ltexprlemrl  7116  ltexprlemru  7118  aptiprleml  7145  aptiprlemu  7146  archpr  7149  cauappcvgprlemm  7151  cauappcvgprlemladdfu  7160  cauappcvgprlemladdfl  7161  caucvgprlemm  7174  caucvgprlemladdfu  7183  caucvgprprlemmu  7201  elreal2  7315  ltresr  7323  axcnre  7363  0re  7435  renepnf  7482  renemnf  7483  ltxrlt  7499  eqlei2  7526  0cnALT  7619  nn1suc  8379  nnne0  8388  xnn0xr  8677  nn0nepnf  8680  elz  8688  elnn0z  8699  elz2  8754  uzind4s  9013  elnn1uz2  9029  qre  9045  fzsn  9414  fz1sbc  9443  elfzp12  9446  fzm1  9447  fz01or  9458  fvinim0ffz  9583  flqidz  9624  ceilqidz  9654  modqmuladdnn0  9706  frec2uzrand  9743  frecuzrdgtcl  9750  fzfig  9768  iseqfveq2  9806  iseqshft2  9810  monoord  9813  iseqsplit  9816  iseqf1olemqval  9824  iseqid2  9847  1exp  9886  bcval  10057  hashennn  10088  zfz1isolem1  10145  zfz1iso  10146  iseqcoll  10147  shftlem  10150  shftfibg  10154  shftfib  10157  shftfn  10158  2shfti  10165  rexuz3  10322  sqrt0rlem  10335  cau3  10447  negfi  10557  sumdc  10642  isumrblem  10660  isummolem2a  10665  fisumss  10675  odd2np1  10779  even2n  10780  oddnn02np1  10786  oddge22np1  10787  evennn02n  10788  evennn2n  10789  nn0enne  10808  divalgmod  10833  lcmgcdlem  10965  cncongr1  10991  1nprm  11002  isprm2  11005  dvdsnprmd  11013  exprmfct  11025  nprmdvds1  11027  coprm  11029  elabgf0  11146  bj-rspgt  11155  cbvrald  11157  decidi  11164  sumdc2  11168  bdssex  11262  bj-inex  11267  bj-intnexr  11269  bj-unexg  11281  bj-d0clsepcl  11289  bj-nnelirr  11317  bj-nn0suc  11328  bj-inf2vnlem1  11334  bj-inf2vnlem2  11335  bj-inf2vnlem3  11336  bj-inf2vnlem4  11337  bj-nn0sucALT  11342  bj-findis  11343  nninfalllemn  11367
  Copyright terms: Public domain W3C validator