Theorem ensym 9009

Description: Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
ensym	⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)

Proof of Theorem ensym

Step	Hyp	Ref	Expression
1		ensymb 9008	. 2 ⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
2	1	biimpi 219	1 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)

This proof depends on syntax axioms:   → wi 4   class class class wbr 5114   ≈ cen 8949

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-er 8703  df-en 8953

This theorem is used by:  ensymi  9010  ensymd  9011  sbthb  9096  domnsym  9101  sdomdomtr  9108  domsdomtr  9110  enen1  9115  enen2  9116  domen1  9117  domen2  9118  sdomen1  9119  sdomen2  9120  domtriord  9121  xpen  9138  pwen  9148  fineqvlem  9236  dif1ennnALT  9247  isfinite2  9268  domunfican  9291  infcntss  9292  wdomen1  9548  wdomen2  9549  unxpwdom2  9560  kardenOLD  9899  finnum  9953  carden2b  9972  fidomtri2  9999  cardmin2  10004  en2eleq  10011  infxpenlem  10016  acnen  10056  acnen2  10058  infpwfien  10065  alephordi  10077  alephinit  10098  dfac12lem2  10147  dfac12r  10149  undjudom  10170  djucomen  10180  djuinf  10191  pwsdompw  10205  infmap2  10219  ackbij1b  10240  cflim2  10265  fin4en1  10311  domfin4  10313  fin23lem25  10326  fin23lem23  10328  enfin1ai  10386  fin67  10397  isfin7-2  10398  fin1a2lem11  10412  axcc2lem  10438  axcclem  10459  numthcor  10496  carden  10553  sdomsdomcard  10562  canthnum  10652  canthwe  10654  canthp1lem2  10656  canthp1  10657  pwxpndom2  10668  gchdjuidm  10671  gchxpidm  10672  gchpwdom  10673  inawinalem  10692  grudomon  10820  isfinite4  14418  hashfn  14431  ramub2  17099  dfod2  19665  sylow2blem1  19721  znhash  21745  hauspwdom  23695  rectbntr0  25027  ovolctb  25686  dyadmbl  25796  eupthfi  30593  padct  33100  karddom  35598  kardsdom  35599  kardexen  35600  derangen  35685  finminlem  36870  domalom  38091  phpreu  38296  pellexlem4  43600  pellexlem5  43601  pellex  43603