Theorem eqcom 2208

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.

Step	Hyp	Ref	Expression
1		bicom 140	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
2	1	albii 1494	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
3		dfcleq 2200	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4		dfcleq 2200	. 2 ⊢ (𝐵 = 𝐴 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐴))
5	2, 3, 4	3bitr4i 212	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 105  ∀wal 1371   = wceq 1373   ∈ wcel 2177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199

This theorem is referenced by:  eqcoms  2209  eqcomi  2210  neqcomd  2211  eqcomd  2212  eqeq2  2216  eqtr2  2225  eqtr3  2226  abeq1  2316  nesym  2422  pm13.181  2459  necom  2461  gencbvex  2821  gencbval  2823  clel5  2914  eqsbc2  3063  dfss  3184  dfss5  3382  rabrsndc  3706  preqr1g  3813  preqr1  3815  invdisj  4044  opthg2  4291  copsex4g  4299  opcom  4303  opeqsn  4305  opeqpr  4306  reusv3  4515  suc11g  4613  opthprc  4734  elxp3  4737  relop  4836  dmopab3  4900  rncoeq  4961  restidsing  5024  dfrel4v  5143  dmsnm  5157  iota1  5255  sniota  5271  dffn5im  5637  fvelrnb  5639  dfimafn2  5641  funimass4  5642  fnsnfv  5651  dmfco  5660  fndmdif  5698  fneqeql  5701  rexrn  5730  ralrn  5731  elrnrexdmb  5733  dffo4  5741  ftpg  5781  fconstfvm  5815  foima2  5833  rexima  5836  ralima  5837  dff13  5850  f1eqcocnv  5873  eusvobj2  5943  f1ocnvfv3  5946  oprabid  5989  eloprabga  6045  ovelimab  6110  dfoprab3  6290  f1o2ndf1  6327  cnvoprab  6333  brtpos2  6350  tpossym  6375  frecsuclem  6505  nntri3or  6592  erth2  6680  brecop  6725  erovlem  6727  ecopovsym  6731  ecopovsymg  6734  xpcomco  6936  mapen  6958  nneneq  6969  supelti  7119  djuf1olem  7170  eldju  7185  omp1eomlem  7211  nninfwlporlemd  7289  exmidontriimlem3  7351  ordpipqqs  7507  addcanprg  7749  ltsrprg  7880  caucvgsrlemcl  7922  caucvgsrlemfv  7924  elreal  7961  ltresr  7972  axcaucvglemcl  8028  axcaucvglemval  8030  addsubeq4  8307  subcan2  8317  negcon1  8344  negcon2  8345  addid0  8465  divmulap2  8769  conjmulap  8822  rerecclap  8823  creur  9052  creui  9053  nndiv  9097  elznn0  9407  zltnle  9438  uzm1  9699  divfnzn  9762  zq  9767  icoshftf1o  10133  iccf1o  10146  fzen  10185  fzneuz  10243  4fvwrd4  10282  qltnle  10408  flqeqceilz  10485  modq0  10496  modqmuladdnn0  10535  addmodlteq  10565  nn0ennn  10600  uzennn  10603  iseqf1olemqcl  10666  iseqf1olemnab  10668  iseqf1olemab  10669  seq3f1olemstep  10681  exp3val  10708  qsqeqor  10817  hashfacen  11003  wrd2ind  11199  cjreb  11252  caucvgrelemrec  11365  minmax  11616  xrnegiso  11648  xrnegcon1d  11650  xrminmax  11651  pwm1geoserap1  11894  dvdsval2  12176  dvdsabseq  12233  dvdsflip  12237  odd2np1  12259  oddm1even  12261  sqoddm1div8z  12272  m1exp1  12287  divalgb  12311  modremain  12315  zeqzmulgcd  12366  dfgcd2  12410  divgcdcoprm0  12498  prm2orodd  12523  hashdvds  12618  oddprmdvds  12752  oddennn  12838  evenennn  12839  gsumval2  13304  grpid  13446  grpinvcnv  13475  grplmulf1o  13481  grpsubeq0  13493  grpsubadd  13495  grplactcnv  13509  isnsg4  13623  eqg0el  13640  conjghm  13687  conjnmzb  13691  dvdsr02  13942  01eq0ring  14026  rmodislmodlem  14187  rspsn  14371  zndvds  14486  znleval  14490  psr1clfi  14525  toponsspwpwg  14569  dmtopon  14570  hmeoimaf1o  14861  txhmeo  14866  limcmpted  15210  ioocosf1o  15401  fsumdvdsmul  15538  gausslemma2dlem0i  15609  lgseisenlem2  15623  lgsquadlem2  15630  2lgslem1c  15642  2lgsoddprmlem2  15658  2lgsoddprm  15665  bj-peano4  16029  pwle2  16076  subctctexmid  16078  pw1nct  16081  exmidsbthrlem  16102  iooref1o  16114  iswomni0  16131