Theorem eqcom 1477

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 520	. . 3 |- ((x e. A <-> x e. B) <-> (x e. B <-> x e. A))
2	1	albii 999	. 2 |- (A.x(x e. A <-> x e. B) <-> A.x(x e. B <-> x e. A))
3		dfcleq 1470	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4		dfcleq 1470	. 2 |- (B = A <-> A.x(x e. B <-> x e. A))
5	2, 3, 4	3bitr4 183	1 |- (A = B <-> B = A)

Syntax hints:   <-> wb 146  A.wal 954   = wceq 956   e. wcel 958

This theorem is referenced by:  eqcoms 1478  eqcomi 1479  eqcomd 1480  eqeq2 1484  eqtr2t 1493  eqtr3t 1494  abeq1 1569  necom 1636  gencbvex 1838  eqvinc 1883  reu7 1935  reu8 1936  sbcco2 1953  dfss 2054  sspsstri 2148  ssequn1 2200  disj4 2317  ssnelpss 2330  preqr1 2481  dtru 2772  copsexg 2792  copsex4g 2794  opprc1b 2796  opeqsn 2802  opeqpr 2803  opthwiener 2807  opabid 2810  euuni 2881  ordtri3or 2979  ordtri2 2982  onmindif2 3061  ordtri2or 3077  suc11 3093  on0eqelt 3124  snsn0non 3125  opelxp 3214  opthprc 3221  elxp3 3224  relop 3275  dmopab3 3322  dmi 3326  rncoeq 3367  iss 3397  intirr 3441  cnvi 3447  coi1 3510  cnvso 3523  fcoi1 3645  fvprc 3721  fnopabfv 3758  fnrnfv 3759  fvelrnb 3760  dfimafn2 3762  funimass4 3763  fnsnfv 3767  dmfco 3773  fvco 3774  fvopabn 3786  elrnopabg 3800  funfvop 3803  dffo4 3820  fconstfv 3849  fvclss 3855  funiunfv 3866  f1fv 3874  f1ocnvfv3 3883  f1oiso 3904  rdglim2 3949  tz7.48lem 3955  eloprabg 4007  oprvalelrn 4039  1st2val 4095  2nd2val 4096  dfoprab5 4115  elrnoprabg 4124  erthdmr 4284  0nelqs 4298  qsid 4301  brecop 4306  ecopoprsym 4310  nneneq 4512  unfilem1 4548  suc11reg 4605  inf3lem2 4614  inf3lem6 4618  aceq5lem2 4736  aceq5lem3 4737  aceq5 4740  kmlem15 4779  brdom7disj 4804  brdom6disj 4805  unxpdomlem 4843  isinfcard 4887  cfeq0 4914  cfsuc 4915  ordpipq 5056  prnmadd 5100  psslinpr 5135  ltexprlem4 5145  suplem2pr 5162  ltsrpr 5186  mulgt0sr 5214  elreal 5250  negcon1 5407  negcon2 5408  negcon1t 5410  negcon2t 5411  leloet 5518  xrleloet 5557  ngtmnftt 5567  lesubadd 5595  add20 5602  leneg 5604  divmul2t 5708  divne0bt 5728  rec11i 5777  conjmult 5797  negeq0t 5806  lerec 5880  arch 6071  elnn0z 6147  elznn0 6149  nn0subt 6161  elnn0nn 6171  zltp1let 6181  zqt 6260  snunioolem 6414  elfzp1 6510  fzneuzt 6518  sqr2irrlem4 6727  cjreb 6781  leabst 6864  abssubne0t 6882  dffsum 6998  dfisum 7191  geoser 7234  reeff1o 7426  nn0ennn 7497  znnen 7502  istps2 7607  cnconst 7780  isgrp 8041  isgrp2i 8076  mulid 8132  nvsubadd 8275  cosh111lem3 8716  efif1lem7 8736  hvsubadd 8933  hiret 8960  hilid 9028  chocuni 9172  omlsilem 9244  shmods 9362  chcon1 9388  chnle 9408  pjoml3 9529  cmbr2 9539  adjsymt 9759  eigorth 9763  dfadj2 9812  adjval2t 9815  cnvadj 9816  dmadjrnb 9830  cnlnadjeu 10010  cnlnssadj 10013  adjbdlnt 10016  pjima 10104  pjin2 10121  pjin3 10122  stadd3 10175  large 10194  cvnbtwn3t 10215  cvnbtwn4t 10216  mddmd 10236  superpos 10281  atnem0 10304  sumdmdi 10342  sumdmdlem 10345  elo 10444  homcard 10539  rcfpfillem2 10587  rcfpfillem2OLD 10588  cmpmon 10743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469

Copyright terms: Public domain