Theorem ensym 8046

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 8045	. 2 ⊢ (𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴)
2	1	biimpi 206	1 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)

Syntax hints:   → wi 4   class class class wbr 4685   ≈ cen 7994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-er 7787  df-en 7998

This theorem is referenced by:  ensymi  8047  ensymd  8048  sbthb  8122  domnsym  8127  sdomdomtr  8134  domsdomtr  8136  enen1  8141  enen2  8142  domen1  8143  domen2  8144  sdomen1  8145  sdomen2  8146  domtriord  8147  xpen  8164  pwen  8174  nneneq  8184  php2  8186  php3  8187  ominf  8213  fineqvlem  8215  en1eqsn  8231  dif1en  8234  enp1i  8236  findcard3  8244  isfinite2  8259  nnsdomg  8260  domunfican  8274  infcntss  8275  fiint  8278  wdomen1  8522  wdomen2  8523  unxpwdom2  8534  karden  8796  finnum  8812  carden2b  8831  fidomtri2  8858  cardmin2  8862  pr2ne  8866  en2eleq  8869  infxpenlem  8874  acnen  8914  acnen2  8916  infpwfien  8923  alephordi  8935  alephinit  8956  dfac12lem2  9004  dfac12r  9006  uncdadom  9031  cdacomen  9041  cdainf  9052  pwsdompw  9064  infmap2  9078  ackbij1b  9099  cflim2  9123  fin4en1  9169  domfin4  9171  fin23lem25  9184  fin23lem23  9186  enfin1ai  9244  fin67  9255  isfin7-2  9256  fin1a2lem11  9270  axcc2lem  9296  axcclem  9317  numthcor  9354  carden  9411  sdomsdomcard  9420  canthnum  9509  canthwe  9511  canthp1lem2  9513  canthp1  9514  pwxpndom2  9525  gchcdaidm  9528  gchxpidm  9529  gchpwdom  9530  inawinalem  9549  grudomon  9677  isfinite4  13191  hashfn  13202  ramub2  15765  dfod2  18027  sylow2blem1  18081  znhash  19955  hauspwdom  21352  rectbntr0  22682  ovolctb  23304  dyadmbl  23414  eupthfi  27183  derangen  31280  finminlem  32437  phpreu  33523  pellexlem4  37713  pellexlem5  37714  pellex  37716