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

Theorem eqcom 2179
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 140 . . 3  |-  ( ( x  e.  A  <->  x  e.  B )  <->  ( x  e.  B  <->  x  e.  A
) )
21albii 1470 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2171 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2171 . 2  |-  ( B  =  A  <->  A. x
( x  e.  B  <->  x  e.  A ) )
52, 3, 43bitr4i 212 1  |-  ( A  =  B  <->  B  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 105   A.wal 1351    = wceq 1353    e. wcel 2148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  eqcoms  2180  eqcomi  2181  neqcomd  2182  eqcomd  2183  eqeq2  2187  eqtr2  2196  eqtr3  2197  abeq1  2287  nesym  2392  pm13.181  2429  necom  2431  gencbvex  2783  gencbval  2785  clel5  2874  eqsbc2  3023  dfss  3143  dfss5  3340  rabrsndc  3659  preqr1g  3764  preqr1  3766  invdisj  3994  opthg2  4236  copsex4g  4244  opcom  4247  opeqsn  4249  opeqpr  4250  reusv3  4457  suc11g  4553  opthprc  4674  elxp3  4677  relop  4773  dmopab3  4836  rncoeq  4896  restidsing  4959  dfrel4v  5076  dmsnm  5090  iota1  5188  sniota  5203  dffn5im  5557  fvelrnb  5559  dfimafn2  5561  funimass4  5562  fnsnfv  5571  dmfco  5580  fndmdif  5617  fneqeql  5620  rexrn  5649  ralrn  5650  elrnrexdmb  5652  dffo4  5660  ftpg  5696  fconstfvm  5730  foima2  5747  rexima  5750  ralima  5751  dff13  5763  f1eqcocnv  5786  eusvobj2  5855  f1ocnvfv3  5858  oprabid  5901  eloprabga  5956  ovelimab  6019  dfoprab3  6186  f1o2ndf1  6223  cnvoprab  6229  brtpos2  6246  tpossym  6271  frecsuclem  6401  nntri3or  6488  erth2  6574  brecop  6619  erovlem  6621  ecopovsym  6625  ecopovsymg  6628  xpcomco  6820  mapen  6840  nneneq  6851  supelti  6995  djuf1olem  7046  eldju  7061  omp1eomlem  7087  nninfwlporlemd  7164  exmidontriimlem3  7216  ordpipqqs  7361  addcanprg  7603  ltsrprg  7734  caucvgsrlemcl  7776  caucvgsrlemfv  7778  elreal  7815  ltresr  7826  axcaucvglemcl  7882  axcaucvglemval  7884  addsubeq4  8159  subcan2  8169  negcon1  8196  negcon2  8197  addid0  8317  divmulap2  8619  conjmulap  8672  rerecclap  8673  creur  8902  creui  8903  nndiv  8946  elznn0  9254  zltnle  9285  uzm1  9544  divfnzn  9607  zq  9612  icoshftf1o  9975  iccf1o  9988  fzen  10026  fzneuz  10084  4fvwrd4  10123  qltnle  10229  flqeqceilz  10301  modq0  10312  modqmuladdnn0  10351  addmodlteq  10381  nn0ennn  10416  uzennn  10419  iseqf1olemqcl  10469  iseqf1olemnab  10471  iseqf1olemab  10472  seq3f1olemstep  10484  exp3val  10505  qsqeqor  10613  hashfacen  10797  cjreb  10856  caucvgrelemrec  10969  minmax  11219  xrnegiso  11251  xrnegcon1d  11253  xrminmax  11254  pwm1geoserap1  11497  dvdsval2  11778  dvdsabseq  11833  dvdsflip  11837  odd2np1  11858  oddm1even  11860  sqoddm1div8z  11871  m1exp1  11886  divalgb  11910  modremain  11914  zeqzmulgcd  11951  dfgcd2  11995  divgcdcoprm0  12081  prm2orodd  12106  hashdvds  12201  oddprmdvds  12332  oddennn  12373  evenennn  12374  grpid  12799  grpinvcnv  12824  grplmulf1o  12830  grpsubeq0  12842  grpsubadd  12844  grplactcnv  12858  dvdsr02  13096  toponsspwpwg  13180  dmtopon  13181  hmeoimaf1o  13474  txhmeo  13479  limcmpted  13792  ioocosf1o  13935  bj-peano4  14356  pwle2  14397  subctctexmid  14399  pw1nct  14401  exmidsbthrlem  14419  iooref1o  14431  iswomni0  14448
  Copyright terms: Public domain W3C validator