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  8683  nn1suc  8707  nnne0  8716  xnn0xr  9013  nn0nepnf  9016  elz  9024  elnn0z  9035  elz2  9090  uzind4s  9353  elnn1uz2  9369  qre  9385  xnn0lenn0nn0  9616  xsubge0  9632  xposdif  9633  xleaddadd  9638  fzsn  9814  fz1sbc  9844  elfzp12  9847  fzm1  9848  fz01or  9859  fvinim0ffz  9986  flqidz  10027  ceilqidz  10057  modqmuladdnn0  10109  frec2uzrand  10146  frecuzrdgtcl  10153  fzfig  10171  seq3fveq2  10210  seq3shft2  10214  monoord  10217  seq3split  10220  iseqf1olemqval  10228  seq3id2  10250  1exp  10290  bcval  10463  hashennn  10494  zfz1isolem1  10551  zfz1iso  10552  seq3coll  10553  shftlem  10556  shftfibg  10560  shftfib  10563  shftfn  10564  2shfti  10571  rexuz3  10730  sqrt0rlem  10743  cau3  10855  negfi  10967  sumdc  11095  sumrbdclem  11113  summodclem2a  11118  fisumss  11129  ef0lem  11293  odd2np1  11497  even2n  11498  oddnn02np1  11504  oddge22np1  11505  evennn02n  11506  evennn2n  11507  nn0enne  11526  divalgmod  11551  lcmgcdlem  11685  cncongr1  11711  1nprm  11722  isprm2  11725  dvdsnprmd  11733  exprmfct  11745  nprmdvds1  11747  coprm  11749  ennnfonelemhom  11855  ctiunctlemudc  11877  fiinopn  12098  istopon  12107  basis2  12142  eltg3  12153  tg2  12156  tgidm  12170  bastop  12171  bastop2  12180  topnex  12182  isopn3  12221  tgrest  12265  cnpval  12294  lmbr  12309  cnconst  12330  txbas  12354  uptx  12370  txdis1cn  12374  cnmpt12  12383  cnmpt22  12390  hmeocnvb  12414  xblm  12513  isxms2  12548  mopni  12578  blssioo  12641  dedekindeulemuub  12691  dedekindeulemeu  12696  dedekindicclemuub  12700  dedekindicclemeu  12705  ivthinclemlm  12708  ivthinclemum  12709  elabgf0  12911  bj-rspgt  12920  cbvrald  12922  decidi  12929  sumdc2  12933  bdssex  13027  bj-inex  13032  bj-intnexr  13034  bj-unexg  13046  bj-d0clsepcl  13050  bj-nnelirr  13078  bj-nn0suc  13089  bj-inf2vnlem1  13095  bj-inf2vnlem2  13096  bj-inf2vnlem3  13097  bj-inf2vnlem4  13098  bj-nn0sucALT  13103  bj-findis  13104  nninfalllemn  13129  trilpolemcl  13157
  Copyright terms: Public domain W3C validator