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

Theorem eleq1 2180
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 2127 . . . 4  |-  ( A  =  B  ->  (
x  =  A  <->  x  =  B ) )
21anbi1d 460 . . 3  |-  ( A  =  B  ->  (
( x  =  A  /\  x  e.  C
)  <->  ( x  =  B  /\  x  e.  C ) ) )
32exbidv 1781 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  A  /\  x  e.  C )  <->  E. x
( x  =  B  /\  x  e.  C
) ) )
4 df-clel 2113 . 2  |-  ( A  e.  C  <->  E. x
( x  =  A  /\  x  e.  C
) )
5 df-clel 2113 . 2  |-  ( B  e.  C  <->  E. x
( x  =  B  /\  x  e.  C
) )
63, 4, 53bitr4g 222 1  |-  ( A  =  B  ->  ( A  e.  C  <->  B  e.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1316   E.wex 1453    e. wcel 1465
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  eleq12  2182  eleq1i  2183  eleq1d  2186  eleq1a  2189  cleqh  2217  nelneq  2218  clelsb3  2222  nfcjust  2246  cleqf  2282  nelne2  2376  neleq1  2384  rgen2a  2463  cbvralf  2625  cbvrexf  2626  cbvreu  2629  cbvrab  2658  eqvisset  2670  ceqsralt  2687  vtoclgaf  2725  vtocl2gaf  2727  vtocl3gaf  2729  rspct  2756  rspc  2757  rspce  2758  rspc2gv  2775  ceqsrexv  2789  ceqsrexbv  2790  clel2  2792  elabgt  2799  elabgf  2800  elrabi  2810  elrabf  2811  elrab3t  2812  ralab2  2821  rexab2  2823  mo2icl  2836  morex  2841  reu2  2845  reu6  2846  rmo4  2850  reu8  2853  reuind  2862  nelrdva  2864  ru  2881  dfsbcq  2884  dfsbcq2  2885  sbc8g  2889  sbcel1v  2943  rmob  2973  difjust  3042  unjust  3044  injust  3046  eldif  3050  dfss2f  3058  uniiunlem  3155  elun  3187  elin  3229  rabn0m  3360  disjne  3386  r19.3rm  3421  r19.9rmv  3424  raaanlem  3438  raaan  3439  ifmdc  3479  elpwg  3488  elpr2  3519  elsn2g  3528  rabsn  3560  tpid3g  3608  snssg  3626  difsn  3627  sssnm  3651  opeq1  3675  opeq2  3676  eluni  3709  elunii  3711  eluniab  3718  elint  3747  elintg  3749  elintab  3752  elintrabg  3754  intss1  3756  eliun  3787  eliin  3788  dfiunv2  3819  opabss  3962  cbvmpt  3993  trel  4003  trss  4005  ssex  4035  intnexr  4046  intexabim  4047  exmidel  4098  euabex  4117  elopab  4150  opelopab2a  4157  frirrg  4242  tz7.2  4246  ordelord  4273  onm  4293  ralxfr2d  4355  rexxfr2d  4356  rabxfrd  4360  reuhypd  4362  ordtriexmid  4407  ordtri2orexmid  4408  ontr2exmid  4410  onsucsssucexmid  4412  onsucelsucexmid  4415  ordsucunielexmid  4416  regexmidlem1  4418  elirr  4426  nordeq  4429  sucprcreg  4434  en2lp  4439  ordsoexmid  4447  ordsuc  4448  onsucuni2  4449  tfis  4467  peano2  4479  findes  4487  limom  4497  opelxp  4539  opeliunxp  4564  opbrop  4588  ssrel  4597  ssrel2  4599  ssrelrel  4609  relopabi  4635  eliunxp  4648  opeliunxp2  4649  ideqg  4660  dmmrnm  4728  dmxpm  4729  elreldm  4735  elrnmptg  4761  elres  4825  resiexg  4834  dfres2  4841  imai  4865  elimasng  4877  issref  4891  xpmlem  4929  xpm  4930  elxp4  4996  elxp5  4997  unielrel  5036  relcnvexb  5048  dmfex  5282  funfveu  5402  funimass4  5440  fvelimab  5445  ssimaex  5450  fvopab3g  5462  fvopab3ig  5463  fvmptssdm  5473  chfnrn  5499  fvelrn  5519  fmpt  5538  ffnfv  5546  fmptco  5554  elunirn  5635  f1elima  5642  cbvriota  5708  acexmidlemab  5736  acexmidlemcase  5737  cbvmpox  5817  eloprabga  5826  resoprab  5835  elrnmpo  5852  ov  5858  ovig  5860  ov6g  5876  ovg  5877  ovelrn  5887  caovimo  5932  fo1stresm  6027  fo2ndresm  6028  elxp6  6035  unielxp  6040  eqop2  6044  dfoprab4  6058  dfoprab4f  6059  fmpox  6066  1stconst  6086  2ndconst  6087  f1o2ndf1  6093  xporderlem  6096  f1od2  6100  disjxp1  6101  opeliunxp2f  6103  dftpos3  6127  dftpos4  6128  tpostpos  6129  smoel  6165  tfr1onlemaccex  6213  tfrcllemaccex  6226  tfrcl  6229  frecabcl  6264  frecsuc  6272  nntri3or  6357  nntri3  6361  nndcel  6364  riinerm  6470  th3qlem1  6499  mapsncnv  6557  elixpsn  6597  dom2lem  6634  fiprc  6677  xpsnen  6683  phplem3g  6718  phpelm  6728  ssfiexmid  6738  domfiexmid  6740  inffiexmid  6768  undifdcss  6779  snon0  6792  f1dmvrnfibi  6800  f1vrnfibi  6801  ordiso2  6888  ctssdclemn0  6963  ctssdc  6966  enumct  6968  finomni  6980  exmidlpo  6983  nnnninf  6991  acfun  7031  ccfunen  7047  elni2  7090  recexnq  7166  recmulnqg  7167  enq0enq  7207  enq0sym  7208  enq0ref  7209  enq0tr  7210  enq0breq  7212  nqnq0pi  7214  nqnq0  7217  prop  7251  prcdnql  7260  prcunqu  7261  prubl  7262  prltlu  7263  prnmaxl  7264  prnminu  7265  prdisj  7268  prarloc  7279  genipv  7285  genpelvl  7288  genpelvu  7289  genprndl  7297  genprndu  7298  distrlem5prl  7362  distrlem5pru  7363  ltexprlemm  7376  ltexprlemdisj  7382  ltexprlemloc  7383  ltexprlemrl  7386  ltexprlemru  7388  aptiprleml  7415  aptiprlemu  7416  archpr  7419  cauappcvgprlemm  7421  cauappcvgprlemladdfu  7430  cauappcvgprlemladdfl  7431  caucvgprlemm  7444  caucvgprlemladdfu  7453  caucvgprprlemmu  7471  elreal2  7606  ltresr  7615  axcnre  7657  axpre-suploclemres  7677  0re  7734  renepnf  7781  renemnf  7782  ltxrlt  7798  eqlei2  7826  0cnALT  7920  sup3exmid  8679  nn1suc  8703  nnne0  8712  xnn0xr  9003  nn0nepnf  9006  elz  9014  elnn0z  9025  elz2  9080  uzind4s  9341  elnn1uz2  9357  qre  9373  xnn0lenn0nn0  9603  xsubge0  9619  xposdif  9620  xleaddadd  9625  fzsn  9801  fz1sbc  9831  elfzp12  9834  fzm1  9835  fz01or  9846  fvinim0ffz  9973  flqidz  10014  ceilqidz  10044  modqmuladdnn0  10096  frec2uzrand  10133  frecuzrdgtcl  10140  fzfig  10158  seq3fveq2  10197  seq3shft2  10201  monoord  10204  seq3split  10207  iseqf1olemqval  10215  seq3id2  10237  1exp  10277  bcval  10450  hashennn  10481  zfz1isolem1  10538  zfz1iso  10539  seq3coll  10540  shftlem  10543  shftfibg  10547  shftfib  10550  shftfn  10551  2shfti  10558  rexuz3  10717  sqrt0rlem  10730  cau3  10842  negfi  10954  sumdc  11082  sumrbdclem  11100  summodclem2a  11105  fisumss  11116  ef0lem  11280  odd2np1  11482  even2n  11483  oddnn02np1  11489  oddge22np1  11490  evennn02n  11491  evennn2n  11492  nn0enne  11511  divalgmod  11536  lcmgcdlem  11670  cncongr1  11696  1nprm  11707  isprm2  11710  dvdsnprmd  11718  exprmfct  11730  nprmdvds1  11732  coprm  11734  ennnfonelemhom  11839  ctiunctlemudc  11861  fiinopn  12082  istopon  12091  basis2  12126  eltg3  12137  tg2  12140  tgidm  12154  bastop  12155  bastop2  12164  topnex  12166  isopn3  12205  tgrest  12249  cnpval  12278  lmbr  12293  cnconst  12314  txbas  12338  uptx  12354  txdis1cn  12358  cnmpt12  12367  cnmpt22  12374  hmeocnvb  12398  xblm  12497  isxms2  12532  mopni  12562  blssioo  12625  dedekindeulemuub  12675  dedekindeulemeu  12680  dedekindicclemuub  12684  dedekindicclemeu  12689  ivthinclemlm  12692  ivthinclemum  12693  elabgf0  12880  bj-rspgt  12889  cbvrald  12891  decidi  12898  sumdc2  12902  bdssex  12996  bj-inex  13001  bj-intnexr  13003  bj-unexg  13015  bj-d0clsepcl  13019  bj-nnelirr  13047  bj-nn0suc  13058  bj-inf2vnlem1  13064  bj-inf2vnlem2  13065  bj-inf2vnlem3  13066  bj-inf2vnlem4  13067  bj-nn0sucALT  13072  bj-findis  13073  nninfalllemn  13098  trilpolemcl  13126
  Copyright terms: Public domain W3C validator