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

Theorem eqcom 2090
Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqcom  |-  ( A  =  B  <->  B  =  A )

Proof of Theorem eqcom
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 bicom 138 . . 3  |-  ( ( x  e.  A  <->  x  e.  B )  <->  ( x  e.  B  <->  x  e.  A
) )
21albii 1404 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2082 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2082 . 2  |-  ( B  =  A  <->  A. x
( x  e.  B  <->  x  e.  A ) )
52, 3, 43bitr4i 210 1  |-  ( A  =  B  <->  B  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 103   A.wal 1287    = wceq 1289    e. wcel 1438
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 1381  ax-gen 1383  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  eqcoms  2091  eqcomi  2092  eqcomd  2093  eqeq2  2097  eqtr2  2106  eqtr3  2107  abeq1  2197  nesym  2300  pm13.181  2337  necom  2339  gencbvex  2665  gencbval  2667  eqsbc3r  2897  dfss  3011  dfss5  3203  rabrsndc  3505  preqr1g  3605  preqr1  3607  invdisj  3831  opthg2  4057  copsex4g  4065  opcom  4068  opeqsn  4070  opeqpr  4071  reusv3  4273  suc11g  4363  opthprc  4477  elxp3  4480  relop  4574  dmopab3  4637  rncoeq  4694  dfrel4v  4869  dmsnm  4883  iota1  4981  sniota  4994  dffn5im  5334  fvelrnb  5336  dfimafn2  5338  funimass4  5339  fnsnfv  5347  dmfco  5356  fndmdif  5388  fneqeql  5391  rexrn  5420  ralrn  5421  elrnrexdmb  5423  dffo4  5431  ftpg  5465  fconstfvm  5497  foima2  5512  rexima  5516  ralima  5517  dff13  5529  f1eqcocnv  5552  eusvobj2  5620  f1ocnvfv3  5623  oprabid  5663  eloprabga  5717  ovelimab  5777  dfoprab3  5943  f1o2ndf1  5975  cnvoprab  5981  brtpos2  5998  tpossym  6023  frecsuclem  6153  nntri3or  6236  erth2  6317  brecop  6362  erovlem  6364  ecopovsym  6368  ecopovsymg  6371  xpcomco  6522  mapen  6542  nneneq  6553  supelti  6676  djuf1olem  6724  eldju  6738  ordpipqqs  6912  addcanprg  7154  ltsrprg  7272  caucvgsrlemcl  7313  caucvgsrlemfv  7315  elreal  7345  ltresr  7355  axcaucvglemcl  7409  axcaucvglemval  7411  addsubeq4  7676  subcan2  7686  negcon1  7713  negcon2  7714  addid0  7830  divmulap2  8117  conjmulap  8170  rerecclap  8171  creur  8391  creui  8392  nndiv  8434  elznn0  8735  zltnle  8766  uzm1  9018  divfnzn  9075  zq  9080  icoshftf1o  9377  iccf1o  9390  fzen  9426  fzneuz  9482  4fvwrd4  9516  qltnle  9622  flqeqceilz  9690  modq0  9701  modqmuladdnn0  9740  addmodlteq  9770  nn0ennn  9805  iseqf1olemqcl  9880  iseqf1olemnab  9882  iseqf1olemab  9883  seq3f1olemstep  9895  exp3val  9922  hashfacen  10206  cjreb  10265  caucvgrelemrec  10377  minmax  10625  pwm1geoserap1  10863  dvdsval2  10881  dvdsabseq  10930  dvdsflip  10934  odd2np1  10955  oddm1even  10957  sqoddm1div8z  10968  m1exp1  10983  divalgb  11007  modremain  11011  zeqzmulgcd  11044  dfgcd2  11085  divgcdcoprm0  11165  prm2orodd  11190  hashdvds  11279  oddennn  11287  evenennn  11288  bj-peano4  11496  exmidsbthrlem  11558
  Copyright terms: Public domain W3C validator