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

Theorem eleq1 2142
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 2091 . . . 4 (𝐴 = 𝐵 → (𝑥 = 𝐴𝑥 = 𝐵))
21anbi1d 453 . . 3 (𝐴 = 𝐵 → ((𝑥 = 𝐴𝑥𝐶) ↔ (𝑥 = 𝐵𝑥𝐶)))
32exbidv 1747 . 2 (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴𝑥𝐶) ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐶)))
4 df-clel 2078 . 2 (𝐴𝐶 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐶))
5 df-clel 2078 . 2 (𝐵𝐶 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐶))
63, 4, 53bitr4g 221 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1285  wex 1422  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  3279  disjne  3304  r19.3rm  3337  r19.9rmv  3340  raaanlem  3354  raaan  3355  elpwg  3398  elpr2  3428  elsn2g  3435  rabsn  3467  tpid3g  3513  snssg  3530  difsn  3531  sssnm  3554  opeq1  3578  opeq2  3579  eluni  3612  elunii  3614  eluniab  3621  elint  3650  elintg  3652  elintab  3655  elintrabg  3657  intss1  3659  eliun  3690  eliin  3691  dfiunv2  3722  opabss  3850  cbvmpt  3880  trel  3890  trss  3892  ssex  3923  intnexr  3934  intexabim  3935  iinexgm  3937  euabex  3988  elopab  4021  opelopab2a  4028  frirrg  4113  tz7.2  4117  ordelord  4144  onm  4164  ralxfr2d  4222  rexxfr2d  4223  rabxfrd  4227  reuhypd  4229  ordtriexmid  4273  ordtri2orexmid  4274  ontr2exmid  4276  onsucsssucexmid  4278  onsucelsucexmid  4281  ordsucunielexmid  4282  regexmidlem1  4284  elirr  4292  nordeq  4295  sucprcreg  4300  en2lp  4305  ordsoexmid  4313  ordsuc  4314  onsucuni2  4315  tfis  4332  peano2  4344  findes  4352  limom  4362  opelxp  4400  opeliunxp  4421  opbrop  4445  ssrel  4454  ssrel2  4456  ssrelrel  4466  relopabi  4491  xpiindim  4501  eliunxp  4503  opeliunxp2  4504  ideqg  4515  dmmrnm  4582  dmxpm  4583  elreldm  4588  elrnmptg  4614  elres  4674  resiexg  4683  dfres2  4688  imai  4711  elimasng  4723  issref  4737  xpmlem  4774  xpm  4775  elxp4  4838  elxp5  4839  unielrel  4875  relcnvexb  4887  cnviinm  4889  dmfex  5110  funfveu  5219  funimass4  5256  fvelimab  5261  ssimaex  5266  fvopab3g  5277  fvopab3ig  5278  fvmptssdm  5287  chfnrn  5310  fvelrn  5330  fmpt  5351  ffnfv  5355  fmptco  5362  elunirn  5437  f1elima  5444  cbvriota  5509  acexmidlemab  5537  acexmidlemcase  5538  cbvmpt2x  5613  eloprabga  5622  resoprab  5628  elrnmpt2  5645  ov  5651  ovig  5653  ov6g  5669  ovg  5670  ovelrn  5680  caovimo  5725  fo1stresm  5819  fo2ndresm  5820  elxp6  5827  unielxp  5831  eqop2  5835  dfoprab4  5849  dfoprab4f  5850  fmpt2x  5857  1stconst  5873  2ndconst  5874  f1o2ndf1  5880  xporderlem  5883  f1od2  5887  dftpos3  5911  dftpos4  5912  tpostpos  5913  smoel  5949  tfr1onlemaccex  5997  tfrcllemaccex  6010  tfrcl  6013  frecabcl  6048  frecsuc  6056  nntri3or  6137  nntri3  6141  nndcel  6144  iinerm  6244  riinerm  6245  th3qlem1  6274  dom2lem  6319  fiprc  6360  xpsnen  6365  phplem3g  6391  phpelm  6401  ssfiexmid  6411  domfiexmid  6413  snon0  6445  f1dmvrnfibi  6452  f1vrnfibi  6453  ordiso2  6505  elni2  6566  recexnq  6642  recmulnqg  6643  enq0enq  6683  enq0sym  6684  enq0ref  6685  enq0tr  6686  enq0breq  6688  nqnq0pi  6690  nqnq0  6693  prop  6727  prcdnql  6736  prcunqu  6737  prubl  6738  prltlu  6739  prnmaxl  6740  prnminu  6741  prdisj  6744  prarloc  6755  genipv  6761  genpelvl  6764  genpelvu  6765  genprndl  6773  genprndu  6774  distrlem5prl  6838  distrlem5pru  6839  ltexprlemm  6852  ltexprlemdisj  6858  ltexprlemloc  6859  ltexprlemrl  6862  ltexprlemru  6864  aptiprleml  6891  aptiprlemu  6892  archpr  6895  cauappcvgprlemm  6897  cauappcvgprlemladdfu  6906  cauappcvgprlemladdfl  6907  caucvgprlemm  6920  caucvgprlemladdfu  6929  caucvgprprlemmu  6947  elreal2  7061  ltresr  7069  axcnre  7109  0re  7181  renepnf  7228  renemnf  7229  ltxrlt  7245  eqlei2  7272  0cnALT  7365  nn1suc  8125  nnne0  8134  xnn0xr  8423  nn0nepnf  8426  elz  8434  elnn0z  8445  elz2  8500  uzind4s  8759  elnn1uz2  8775  qre  8791  fzsn  9160  fz1sbc  9189  elfzp12  9192  fzm1  9193  fz01or  9204  fvinim0ffz  9327  flqidz  9368  ceilqidz  9398  modqmuladdnn0  9450  frec2uzrand  9487  frecuzrdgtcl  9494  fzfig  9512  iseqfveq2  9544  iseqshft2  9548  monoord  9551  iseqsplit  9554  iseqid2  9564  1exp  9602  bcval  9773  sizeennn  9804  shftlem  9842  shftfibg  9846  shftfib  9849  shftfn  9850  2shfti  9857  rexuz3  10014  sqrt0rlem  10027  cau3  10139  negfi  10248  sumdc  10333  isumrblem  10337  odd2np1  10417  even2n  10418  oddnn02np1  10424  oddge22np1  10425  evennn02n  10426  evennn2n  10427  nn0enne  10446  divalgmod  10471  lcmgcdlem  10603  cncongr1  10629  1nprm  10640  isprm2  10643  dvdsnprmd  10651  exprmfct  10663  nprmdvds1  10665  coprm  10667  elabgf0  10738  bj-rspgt  10747  cbvrald  10749  decidi  10756  sumdc2  10760  bdssex  10851  bj-inex  10856  bj-intnexr  10858  bj-unexg  10870  bj-d0clsepcl  10878  bj-nnelirr  10906  bj-nn0suc  10917  bj-inf2vnlem1  10923  bj-inf2vnlem2  10924  bj-inf2vnlem3  10925  bj-inf2vnlem4  10926  bj-nn0sucALT  10931  bj-findis  10932
  Copyright terms: Public domain W3C validator