Theorem ensymd 6782

Description: Symmetry of equinumerosity. Deduction form of ensym 6780. (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 6780	. 2 |- ( A ~~ B -> B ~~ A )
3	1, 2	syl 14	1 |- ( ph -> B ~~ A )

Syntax hints:   -> wi 4   class class class wbr 4003   ~~ cen 6737

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-er 6534  df-en 6740

This theorem is referenced by:  f1imaeng  6791  f1imaen2g  6792  en2sn  6812  xpdom3m  6833  phplem4  6854  phplem4dom  6861  php5dom  6862  phpm  6864  phplem4on  6866  dif1en  6878  dif1enen  6879  fisbth  6882  fin0  6884  fin0or  6885  fientri3  6913  unsnfidcex  6918  unsnfidcel  6919  fiintim  6927  fisseneq  6930  f1ofi  6941  endjusym  7094  eninl  7095  eninr  7096  pm54.43  7188  djuen  7209  dju1en  7211  djuassen  7215  xpdjuen  7216  uzenom  10424  hashennnuni  10758  hashennn  10759  hashcl  10760  hashfz1  10762  hashen  10763  fihashfn  10779  fihashdom  10782  hashunlem  10783  zfz1iso  10820  summodclem2  11389  zsumdc  11391  prodmodclem2  11584  zproddc  11586  ennnfonelemen  12421  exmidunben  12426  ctinfom  12428  ctinf  12430  pwf1oexmid  14719  sbthom  14744