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

Theorem eleq1 2203
 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 2150 . . . 4 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21anbi1d 461 . . 3 (𝐴 = 𝐵 → ((𝑥 = 𝐴𝑥𝐶) ↔ (𝑥 = 𝐵𝑥𝐶)))
32exbidv 1798 . 2 (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴𝑥𝐶) ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐶)))
4 df-clel 2136 . 2 (𝐴𝐶 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐶))
5 df-clel 2136 . 2 (𝐵𝐶 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐶))
63, 4, 53bitr4g 222 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332  ∃wex 1469   ∈ wcel 1481 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136 This theorem is referenced by:  eleq12  2205  eleq1i  2206  eleq1d  2209  eleq1a  2212  cleqh  2240  nelneq  2241  clelsb3  2245  nfcjust  2270  cleqf  2306  nelne2  2400  neleq1  2408  rgen2a  2490  cbvralf  2652  cbvrexf  2653  cbvreu  2656  cbvrab  2688  eqvisset  2700  ceqsralt  2717  vtoclgaf  2755  vtocl2gaf  2757  vtocl3gaf  2759  rspct  2787  rspc  2788  rspce  2789  rspc2gv  2806  ceqsrexv  2820  ceqsrexbv  2821  clel2  2823  elabgt  2830  elabgf  2831  elrabi  2842  elrabf  2843  elrab3t  2844  ralab2  2853  rexab2  2855  mo2icl  2868  morex  2873  reu2  2877  reu6  2878  rmo4  2882  reu8  2885  reuind  2894  nelrdva  2896  ru  2913  dfsbcq  2916  dfsbcq2  2917  sbc8g  2921  sbcel1v  2976  rmob  3006  difjust  3078  unjust  3080  injust  3082  eldif  3086  dfss2f  3094  uniiunlem  3191  elun  3223  elin  3265  rabn0m  3396  disjne  3422  r19.3rm  3457  r19.9rmv  3460  raaanlem  3474  raaan  3475  ifmdc  3515  elpwg  3524  elpr2  3555  elsn2g  3566  rabsn  3599  tpid3g  3647  snssg  3665  difsn  3666  sssnm  3690  opeq1  3714  opeq2  3715  eluni  3748  elunii  3750  eluniab  3757  elint  3786  elintg  3788  elintab  3791  elintrabg  3793  intss1  3795  eliun  3826  eliin  3827  dfiunv2  3858  opabss  4001  cbvmpt  4032  trel  4042  trss  4044  ssex  4074  intnexr  4085  intexabim  4086  exmidel  4137  euabex  4156  elopab  4189  opelopab2a  4196  frirrg  4281  tz7.2  4285  ordelord  4312  onm  4332  ralxfr2d  4394  rexxfr2d  4395  rabxfrd  4399  reuhypd  4401  ordtriexmid  4446  ordtri2orexmid  4447  ontr2exmid  4449  onsucsssucexmid  4451  onsucelsucexmid  4454  ordsucunielexmid  4455  regexmidlem1  4457  elirr  4465  nordeq  4468  sucprcreg  4473  en2lp  4478  ordsoexmid  4486  ordsuc  4487  onsucuni2  4488  tfis  4506  peano2  4518  findes  4526  limom  4536  opelxp  4578  opeliunxp  4603  opbrop  4627  ssrel  4636  ssrel2  4638  ssrelrel  4648  relopabi  4674  eliunxp  4687  opeliunxp2  4688  ideqg  4699  dmmrnm  4767  dmxpm  4768  elreldm  4774  elrnmptg  4800  elres  4864  resiexg  4873  dfres2  4880  imai  4904  elimasng  4916  issref  4930  xpmlem  4968  xpm  4969  elxp4  5035  elxp5  5036  unielrel  5075  relcnvexb  5087  dmfex  5321  funfveu  5443  funimass4  5481  fvelimab  5486  ssimaex  5491  fvopab3g  5503  fvopab3ig  5504  fvmptssdm  5514  chfnrn  5540  fvelrn  5560  fmpt  5579  ffnfv  5587  fmptco  5595  elunirn  5676  f1elima  5683  cbvriota  5749  acexmidlemab  5777  acexmidlemcase  5778  cbvmpox  5858  eloprabga  5867  resoprab  5876  elrnmpo  5893  ov  5899  ovig  5901  ov6g  5917  ovg  5918  ovelrn  5928  caovimo  5973  fo1stresm  6068  fo2ndresm  6069  elxp6  6076  unielxp  6081  eqop2  6085  dfoprab4  6099  dfoprab4f  6100  fmpox  6107  1stconst  6127  2ndconst  6128  f1o2ndf1  6134  xporderlem  6137  f1od2  6141  disjxp1  6142  opeliunxp2f  6144  dftpos3  6168  dftpos4  6169  tpostpos  6170  smoel  6206  tfr1onlemaccex  6254  tfrcllemaccex  6267  tfrcl  6270  frecabcl  6305  frecsuc  6313  nntri3or  6398  nntri3  6402  nndcel  6405  riinerm  6511  th3qlem1  6540  mapsncnv  6598  elixpsn  6638  dom2lem  6675  fiprc  6718  xpsnen  6724  phplem3g  6759  phpelm  6769  ssfiexmid  6779  domfiexmid  6781  inffiexmid  6809  undifdcss  6821  snon0  6834  f1dmvrnfibi  6842  f1vrnfibi  6843  ordiso2  6930  ctssdclemn0  7005  ctssdc  7008  enumct  7010  finomni  7022  exmidlpo  7025  nnnninf  7033  acfun  7083  pw1ne1  7100  onntri35  7108  ccfunen  7116  cc2lem  7118  elni2  7166  recexnq  7242  recmulnqg  7243  enq0enq  7283  enq0sym  7284  enq0ref  7285  enq0tr  7286  enq0breq  7288  nqnq0pi  7290  nqnq0  7293  prop  7327  prcdnql  7336  prcunqu  7337  prubl  7338  prltlu  7339  prnmaxl  7340  prnminu  7341  prdisj  7344  prarloc  7355  genipv  7361  genpelvl  7364  genpelvu  7365  genprndl  7373  genprndu  7374  distrlem5prl  7438  distrlem5pru  7439  ltexprlemm  7452  ltexprlemdisj  7458  ltexprlemloc  7459  ltexprlemrl  7462  ltexprlemru  7464  aptiprleml  7491  aptiprlemu  7492  archpr  7495  cauappcvgprlemm  7497  cauappcvgprlemladdfu  7506  cauappcvgprlemladdfl  7507  caucvgprlemm  7520  caucvgprlemladdfu  7529  caucvgprprlemmu  7547  elreal2  7682  ltresr  7691  axcnre  7733  axpre-suploclemres  7753  0re  7810  renepnf  7857  renemnf  7858  ltxrlt  7874  eqlei2  7902  0cnALT  7996  sup3exmid  8759  nn1suc  8783  nnne0  8792  xnn0xr  9089  nn0nepnf  9092  elz  9100  elnn0z  9111  elz2  9166  uzind4s  9432  elnn1uz2  9448  qre  9464  elpqb  9488  xnn0lenn0nn0  9698  xsubge0  9714  xposdif  9715  xleaddadd  9720  fzsn  9897  fz1sbc  9927  elfzp12  9930  fzm1  9931  fz01or  9942  fvinim0ffz  10069  flqidz  10110  ceilqidz  10140  modqmuladdnn0  10192  frec2uzrand  10229  frecuzrdgtcl  10236  fzfig  10254  seq3fveq2  10293  seq3shft2  10297  monoord  10300  seq3split  10303  iseqf1olemqval  10311  seq3id2  10333  1exp  10373  bcval  10547  hashennn  10578  zfz1isolem1  10635  zfz1iso  10636  seq3coll  10637  shftlem  10640  shftfibg  10644  shftfib  10647  shftfn  10648  2shfti  10655  rexuz3  10814  sqrt0rlem  10827  cau3  10939  negfi  11051  sumdc  11179  sumrbdclem  11198  summodclem2a  11202  fisumss  11213  prodrbdclem  11392  prodmodclem2a  11397  ef0lem  11423  odd2np1  11626  even2n  11627  oddnn02np1  11633  oddge22np1  11634  evennn02n  11635  evennn2n  11636  nn0enne  11655  divalgmod  11680  lcmgcdlem  11814  cncongr1  11840  1nprm  11851  isprm2  11854  dvdsnprmd  11862  exprmfct  11874  nprmdvds1  11876  coprm  11878  ennnfonelemhom  11984  ctiunctlemudc  12006  fiinopn  12230  istopon  12239  basis2  12274  eltg3  12285  tg2  12288  tgidm  12302  bastop  12303  bastop2  12312  topnex  12314  isopn3  12353  tgrest  12397  cnpval  12426  lmbr  12441  cnconst  12462  txbas  12486  uptx  12502  txdis1cn  12506  cnmpt12  12515  cnmpt22  12522  hmeocnvb  12546  xblm  12645  isxms2  12680  mopni  12710  blssioo  12773  dedekindeulemuub  12823  dedekindeulemeu  12828  dedekindicclemuub  12832  dedekindicclemeu  12837  ivthinclemlm  12840  ivthinclemum  12841  elabgf0  13175  bj-rspgt  13184  cbvrald  13186  decidi  13193  sumdc2  13197  bdssex  13291  bj-inex  13296  bj-intnexr  13298  bj-unexg  13310  bj-d0clsepcl  13314  bj-nnelirr  13342  bj-nn0suc  13353  bj-inf2vnlem1  13359  bj-inf2vnlem2  13360  bj-inf2vnlem3  13361  bj-inf2vnlem4  13362  bj-nn0sucALT  13367  bj-findis  13368  nninfalllemn  13396  trilpolemcl  13426
 Copyright terms: Public domain W3C validator