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

Theorem eqcom 2024
Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqcom

Proof of Theorem eqcom
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bicom 128 . . 3
21albii 1339 . 2
3 dfcleq 2016 . 2
4 dfcleq 2016 . 2
52, 3, 43bitr4i 201 1
Colors of variables: wff set class
Syntax hints:   wb 98  wal 1226   wceq 1228   wcel 1374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  eqcoms  2025  eqcomi  2026  eqcomd  2027  eqeq2  2031  eqtr2  2040  eqtr3  2041  abeq1  2129  nesym  2228  pm13.181  2265  necom  2267  gencbvex  2577  gencbval  2579  eqsbc3r  2796  dfss  2909  dfss5  3119  disj4im  3253  ssnelpss  3266  rabrsndc  3412  preqr1g  3511  preqr1  3513  invdisj  3733  opthg2  3950  copsex4g  3958  opcom  3961  opeqsn  3963  opeqpr  3964  reusv3  4142  suc11g  4219  dtruex  4221  opthprc  4318  elxp3  4321  relop  4413  dmopab3  4475  rncoeq  4532  dfrel4v  4699  dmsnm  4713  iota1  4808  sniota  4821  dffn5im  5144  fvelrnb  5146  dfimafn2  5148  funimass4  5149  fnsnfv  5157  dmfco  5166  fndmdif  5197  fneqeql  5200  rexrn  5229  ralrn  5230  elrnrexdmb  5232  dffo4  5240  ftpg  5272  fconstfvm  5304  rexima  5319  ralima  5320  dff13  5332  f1eqcocnv  5356  eusvobj2  5422  f1ocnvfv3  5425  oprabid  5461  eloprabga  5514  ovelimab  5574  dfoprab3  5740  f1o2ndf1  5772  brtpos2  5788  tpossym  5813  frec0g  5902  frecsuclem3  5906  nntri3or  5987  erth2  6062  brecop  6107  erovlem  6109  ecopovsym  6113  ecopovsymg  6116  ordpipqqs  6233  addcanprg  6453  ltsrprg  6494  elreal  6541  ltresr  6550  addsubeq4  6813  subcan2  6822  negcon1  6849  negcon2  6850  bj-peano4  7177
  Copyright terms: Public domain W3C validator