Theorem ensymd 6875

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

Hypothesis

Ref	Expression
ensymd.1	|- ( ph -> A ~~ B )

Assertion

Ref	Expression
ensymd	|- ( ph -> B ~~ A )

Proof of Theorem ensymd

Step	Hyp	Ref	Expression
1		ensymd.1	. 2 |- ( ph -> A ~~ B )
2		ensym 6873	. 2 |- ( A ~~ B -> B ~~ A )
3	1, 2	syl 14	1 |- ( ph -> B ~~ A )

Syntax hints:   -> wi 4   class class class wbr 4044   ~~ cen 6825

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-un 4480

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-res 4687  df-ima 4688  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-er 6620  df-en 6828

This theorem is referenced by:  f1imaeng  6884  f1imaen2g  6885  en2sn  6905  xpdom3m  6929  phplem4  6952  phplem4dom  6959  php5dom  6960  phpm  6962  phplem4on  6964  dif1en  6976  dif1enen  6977  fisbth  6980  fin0  6982  fin0or  6983  fientri3  7012  unsnfidcex  7017  unsnfidcel  7018  fiintim  7028  fisseneq  7031  f1ofi  7045  endjusym  7198  eninl  7199  eninr  7200  pm54.43  7298  djuen  7323  dju1en  7325  djuassen  7329  xpdjuen  7330  uzenom  10570  hashennnuni  10924  hashennn  10925  hashcl  10926  hashfz1  10928  hashen  10929  fihashfn  10945  fihashdom  10948  hashunlem  10949  zfz1iso  10986  summodclem2  11693  zsumdc  11695  prodmodclem2  11888  zproddc  11890  4sqlem11  12724  ennnfonelemen  12792  exmidunben  12797  ctinfom  12799  ctinf  12801  isnzr2  13946  znfi  14417  znhash  14418  pwf1oexmid  15936  nnnninfen  15958  sbthom  15965