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

Theorem eqcom 2042
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 1359 . 2 (∀𝑥(𝑥𝐴𝑥𝐵) ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
3 dfcleq 2034 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 dfcleq 2034 . 2 (𝐵 = 𝐴 ↔ ∀𝑥(𝑥𝐵𝑥𝐴))
52, 3, 43bitr4i 201 1 (𝐴 = 𝐵𝐵 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1241   = wceq 1243  wcel 1393
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 1336  ax-gen 1338  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  eqcoms  2043  eqcomi  2044  eqcomd  2045  eqeq2  2049  eqtr2  2058  eqtr3  2059  abeq1  2147  nesym  2250  pm13.181  2287  necom  2289  gencbvex  2600  gencbval  2602  eqsbc3r  2819  dfss  2932  dfss5  3142  disj4im  3276  ssnelpss  3289  rabrsndc  3438  preqr1g  3537  preqr1  3539  invdisj  3759  opthg2  3976  copsex4g  3984  opcom  3987  opeqsn  3989  opeqpr  3990  reusv3  4192  suc11g  4281  dtruex  4283  opthprc  4391  elxp3  4394  relop  4486  dmopab3  4548  rncoeq  4605  dfrel4v  4772  dmsnm  4786  iota1  4881  sniota  4894  dffn5im  5219  fvelrnb  5221  dfimafn2  5223  funimass4  5224  fnsnfv  5232  dmfco  5241  fndmdif  5272  fneqeql  5275  rexrn  5304  ralrn  5305  elrnrexdmb  5307  dffo4  5315  ftpg  5347  fconstfvm  5379  rexima  5394  ralima  5395  dff13  5407  f1eqcocnv  5431  eusvobj2  5498  f1ocnvfv3  5501  oprabid  5537  eloprabga  5591  ovelimab  5651  dfoprab3  5817  f1o2ndf1  5849  brtpos2  5866  tpossym  5891  frecsuclem3  5990  nntri3or  6072  erth2  6151  brecop  6196  erovlem  6198  ecopovsym  6202  ecopovsymg  6205  xpcomco  6300  nneneq  6320  ordpipqqs  6470  addcanprg  6712  ltsrprg  6830  caucvgsrlemcl  6871  caucvgsrlemfv  6873  elreal  6903  ltresr  6913  axcaucvglemcl  6967  axcaucvglemval  6969  addsubeq4  7224  subcan2  7234  negcon1  7261  negcon2  7262  divmulap2  7653  conjmulap  7703  rerecclap  7704  creur  7909  creui  7910  nndiv  7952  elznn0  8258  zltnle  8289  uzm1  8501  divfnzn  8554  zq  8559  icoshftf1o  8857  iccf1o  8870  fzen  8905  fzneuz  8961  4fvwrd4  8995  qltnle  9099  flqeqceilz  9158  modq0  9169  nn0ennn  9207  cjreb  9464  caucvgrelemrec  9576  bj-peano4  10078
  Copyright terms: Public domain W3C validator