Theorem ensymd 6905

Description: Symmetry of equinumerosity. Deduction form of ensym 6903. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ensymd.1	⊢ (𝜑 → 𝐴 ≈ 𝐵)

Assertion

Ref	Expression
ensymd	⊢ (𝜑 → 𝐵 ≈ 𝐴)

Proof of Theorem ensymd

Step	Hyp	Ref	Expression
1		ensymd.1	. 2 ⊢ (𝜑 → 𝐴 ≈ 𝐵)
2		ensym 6903	. 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐵 ≈ 𝐴)

Syntax hints:   → wi 4   class class class wbr 4062   ≈ cen 6855

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-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-er 6650  df-en 6858

This theorem is referenced by:  f1imaeng  6914  f1imaen2g  6915  en2sn  6936  xpdom3m  6961  phplem4  6984  phplem4dom  6991  php5dom  6992  phpm  6995  phplem4on  6997  dif1en  7009  dif1enen  7010  fisbth  7013  fin0  7015  fin0or  7016  fientri3  7045  unsnfidcex  7050  unsnfidcel  7051  fiintim  7061  fisseneq  7064  f1ofi  7078  endjusym  7231  eninl  7232  eninr  7233  pm54.43  7331  djuen  7361  dju1en  7363  djuassen  7367  xpdjuen  7368  uzenom  10614  hashennnuni  10968  hashennn  10969  hashcl  10970  hashfz1  10972  hashen  10973  fihashfn  10989  fihashdom  10992  hashunlem  10993  zfz1iso  11030  summodclem2  11859  zsumdc  11861  prodmodclem2  12054  zproddc  12056  4sqlem11  12890  ennnfonelemen  12958  exmidunben  12963  ctinfom  12965  ctinf  12967  isnzr2  14113  znfi  14584  znhash  14585  usgrsizedgen  15976  pwf1oexmid  16276  nnnninfen  16298  sbthom  16305