Theorem eqcom 1480

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 522	. . 3 |- ((x e. A <-> x e. B) <-> (x e. B <-> x e. A))
2	1	albii 1001	. 2 |- (A.x(x e. A <-> x e. B) <-> A.x(x e. B <-> x e. A))
3		dfcleq 1473	. 2 |- (A = B <-> A.x(x e. A <-> x e. B))
4		dfcleq 1473	. 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 956   = wceq 958   e. wcel 960

This theorem is referenced by:  eqcoms 1481  eqcomi 1482  eqcomd 1483  eqeq2 1487  eqtr2t 1496  eqtr3t 1497  abeq1 1572  necom 1639  gencbvex 1841  eqvinc 1886  reu7 1938  reu8 1939  sbcco2 1956  dfss 2057  sspsstri 2151  ssequn1 2203  disj4 2321  ssnelpss 2334  preqr1 2485  dtru 2778  copsexg 2798  copsex4g 2800  opprc1b 2802  opeqsn 2808  opeqpr 2809  opthwiener 2813  opabid 2816  euuni 2887  ordtri3or 2985  ordtri2 2988  onmindif2 3067  ordtri2or 3083  suc11 3099  on0eqelt 3130  snsn0non 3131  opelxp 3220  opthprc 3227  elxp3 3230  relop 3281  dmopab3 3328  dmi 3332  rncoeq 3373  iss 3403  intirr 3447  cnvi 3453  coi1 3516  cnvso 3529  fcoi1 3651  fvprc 3727  fnopabfv 3764  fnrnfv 3765  fvelrnb 3766  dfimafn2 3768  funimass4 3769  fnsnfv 3773  dmfco 3779  fvco 3780  fvopabn 3792  elrnopabg 3806  funfvop 3809  dffo4 3826  fconstfv 3855  fvclss 3861  funiunfv 3872  f1fv 3880  f1ocnvfv3 3889  f1oiso 3910  rdglim2 3955  tz7.48lem 3961  eloprabg 4013  oprvalelrn 4045  1st2val 4101  2nd2val 4102  dfoprab5 4121  elrnoprabg 4130  erthdmr 4290  0nelqs 4304  qsid 4307  brecop 4312  ecopoprsym 4316  nneneq 4518  unfilem1 4560  suc11reg 4614  inf3lem2 4623  inf3lem6 4627  aceq5lem2 4746  aceq5lem3 4747  aceq5 4750  kmlem15 4789  brdom7disj 4814  brdom6disj 4815  unxpdomlem 4854  isinfcard 4898  cfeq0 4926  cfsuc 4927  ordpipq 5068  prnmadd 5112  psslinpr 5147  ltexprlem4 5157  suplem2pr 5174  ltsrpr 5198  mulgt0sr 5226  elreal 5262  negcon1 5419  negcon2 5420  negcon1t 5422  negcon2t 5423  leloet 5530  xrleloet 5569  ngtmnftt 5579  lesubadd 5607  add20 5614  leneg 5616  divmul2t 5720  divne0bt 5735  rec11i 5779  conjmult 5799  negeq0t 5808  lerec 5882  arch 6073  elnn0z 6149  elznn0 6151  nn0subt 6163  elnn0nn 6173  zltp1let 6183  zqt 6261  snunioolem 6415  elfzp1 6511  fzneuzt 6519  sqr2irrlem4 6728  cjreb 6781  leabst 6864  abssubne0t 6882  dffsum 6998  dfisum 7191  geoser 7234  reeff1o 7426  nn0ennn 7498  znnen 7503  istps2 7608  cnconst 7777  isgrp 8038  isgrp2i 8072  mulid 8128  nvsubadd 8271  cosh111lem3 8711  efif1lem7 8731  hvsubadd 8928  hiret 8955  hilid 9023  chocuni 9167  omlsilem 9239  shmods 9357  chcon1 9383  chnle 9403  pjoml3 9524  cmbr2 9534  adjsymt 9754  eigorth 9758  dfadj2 9807  adjval2t 9810  cnvadj 9811  dmadjrnb 9825  cnlnadjeu 10005  cnlnssadj 10008  adjbdlnt 10011  pjima 10099  pjin2 10116  pjin3 10117  stadd3 10170  large 10189  cvnbtwn3t 10210  cvnbtwn4t 10211  mddmd 10231  superpos 10276  atnem0 10299  sumdmdi 10337  sumdmdlem 10340  elo 10439  homcard 10525  rcfpfillem2 10564  cmpmon 10714

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain