Theorem eqcom 1886

Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41.

Assertion

Ref	Expression
eqcom	|- (A = B <-> B = A)

Proof of Theorem eqcom

Step	Hyp	Ref	Expression
1		bicom 579	. . 3 |- ((x e. A <-> x e. B) <-> (x e. B <-> x e. A))
2	1	albii 1346	. 2 |- (A.x(x e. A <-> x e. B) <-> A.x(x e. B <-> x e. A))
3		dfcleq 1878	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4		dfcleq 1878	. 2 |- (B = A <-> A.x(x e. B <-> x e. A))
5	2, 3, 4	3bitr4i 200	1 |- (A = B <-> B = A)

Syntax hints:   <-> wb 163  A.wal 1296   = wceq 1298   e. wcel 1300

This theorem is referenced by:  eqcoms 1887  eqcomi 1888  eqcomd 1889  eqeq2 1893  eqtr2 1905  eqtr2OLD 1906  eqtr3 1907  abeq1 2000  pm13.181 2086  necom 2094  gencbvex 2334  gencbvexOLD 2335  eqvincOLD 2388  reu7 2447  reu8 2448  sbcco2OLD 2469  eqsbc3r 2507  dfss 2606  sspsstri 2711  ssequn1OLD 2776  disj4 2922  ssnelpss 2937  preqr1 3152  dtruALT 3517  copsexg 3537  copsexgOLD 3538  copsex4g 3540  opprc1b 3542  opcom 3547  opeqsn 3549  opeqpr 3550  opthwiener 3554  opabidOLD 3558  ordtri3orOLD 3692  ordtri2 3696  ordtri2orOLD 3767  suc11 3773  on0eqel 3787  snsn0non 3788  snsn0nonOLD 3789  euuni 3807  eufromeq3 3830  onmindif2 3893  opelxpOLD 4037  opthprc 4046  elxp3 4049  relop 4113  dmopab3 4169  dmiOLD 4173  rncoeq 4217  issOLD 4255  intirrOLD 4313  cnviOLD 4321  xpcan 4348  xpcan2 4350  dmsnn0 4362  coi1 4413  cnvso 4428  iunfopabOLD 4543  fcoi1OLD 4585  fvprc 4678  dffn5 4717  fnrnfv 4718  fvelrnb 4719  dfimafn2 4721  funimass4 4722  fnsnfv 4728  dmfco 4735  fvco 4736  fvopabn 4749  elrnopabg 4773  funfvop 4776  dffo4 4793  fconstfv 4825  fvclss 4831  funiunfv 4842  dff13 4850  f1ocnvfv3 4859  f1oiso 4881  eloprabg 4936  oprvelrn 4969  dfoprab3s 5055  elrnoprabg 5066  rdglim2 5157  tz7.48lem 5164  erthdmr 5342  qsid 5360  brecop 5365  ecopoprsym 5369  nneneq 5606  unfilem1 5641  suc11reg 5710  inf3lem2 5720  inf3lem6 5724  aceq5lem2 5898  aceq5lem3 5899  aceq5 5902  kmlem15 5941  brdom7disj 5966  brdom6disj 5967  unxpdomlem 5995  isinfcard 6035  cfeq0 6062  cfsuc 6063  ordpipq 6208  prnmadd 6252  psslinpr 6287  ltexprlem4 6297  suplem2pr 6314  ltsrpr 6338  mulgt0sr 6366  elreal 6402  negcon1i 6567  negcon2i 6568  negcon1 6570  negcon2 6571  leloe 6688  xrleloe 6732  ngtmnft 6742  lesubaddiOLD 6772  add20i 6782  lenegi 6784  divmul2 6897  divne0b 6911  rec11ii 6953  conjmul 6975  negeq0 6984  lereci 7063  arch 7280  elnn0z 7356  elznn0 7358  nn0sub 7370  elnn0nn 7380  zltp1le 7390  zq 7440  modirr 7522  snunioolem 7583  fzen 7664  elfzp1 7683  fzneuz 7697  sqr2irrlem4 7977  cjrebi 8031  leabs 8115  abssubne0 8134  dffsum 8258  dfisum 8452  geoseri 8496  reeff1o 8691  nn0ennn 8766  znnen 8771  istps2 8876  cnconst 9057  isgrp 9321  isgrp2i 9360  mulid 9440  nvsubadd 9607  cosh111lem3 10070  efif1lem7 10090  twpar2 10149  filrn 10293  limfil 10297  usinuniop 10341  opidon 10369  rngmgmbs4 10401  hvsubaddi 10565  hire 10593  hilid 10661  chocunii 10805  omlsilem 10877  shmodsi 10995  chcon1i 11021  chnlei 11041  pjoml3i 11162  cmbr2i 11172  adjsym 11396  eigorthi 11400  dfadj2 11449  adjval2 11452  cnvadj 11453  dmadjrnb 11467  cnlnadjeui 11647  cnlnssadj 11650  adjbdln 11653  pjimai 11748  pjin2i 11766  pjin3i 11767  stadd3i 11820  largei 11839  cvnbtwn3 11860  cvnbtwn4 11861  mddmd2 11881  superpos 11926  atnem0 11949  sumdmdii 11987  sumdmdlem 11990  addltmulALT 12018  bnj512 12519  bnj549 13275  bnj965 13346  bnj964 13347  elnn00nn 13602  fz1eqblem 13608  divalglem4 13699  divalglem8 13703  divalgb 13707  divalgmod 13709  dfon2lem5 13853  dfon2lem8 13856  soseq 13955  sltval2 13997  sltintdifex 14004  axbday 14012  axfelem12 14042  axfelem15 14045  axfelem16 14046  ellimits 14079  elo 14342  surjsec2 14467  repcpwti 14503  supdef 14604  dffprod 14670  gaplc 14731  curgrpact 14735  imtr 14762  homcard 14893  rcfpfillem2 14929  limfillem1 14938  bsi2 14992  dualded 15132  dualcat2 15133  cmpmon 15164  iepiclem 15172  elicc3 15362  finminlem 15367  fictb 15371  opncldf1 15402  opncldf3 15404  opnregcld 15415  cldregopn 15416  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  reconnlem1 15446  ssref 15492  topfneec 15501  refssfne 15504  rnelfmlem 15592  filclus 15605  fimaxre 15774  addsubeq4 15778  mod0 15800  sdc 15811  fdc 15812  heiborlem8 15962  phtpycom 16050  phtpycolem2 16052  phtpcer 16062  pcohtpylem2 16081  0ring 16175  smprngpr 16200  isfldidl 16216  isfldidl2 16217  erdisj3 16266  pm13.181OLD 16372  eqsbc3rVD 16664  strdif 16719  latnle 16880  opcon1b 16925  omllaw2 16965  cmtbr2 16974  leatom 17005  glbconx 17029  ps2 17079  poml4 17361

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain