Theorem ensymd 6629

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

Syntax hints:   -> wi 4   class class class wbr 3893   ~~ cen 6584

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089  ax-un 4313

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-id 4173  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-er 6381  df-en 6587

This theorem is referenced by:  f1imaeng  6638  f1imaen2g  6639  en2sn  6659  xpdom3m  6679  phplem4  6700  phplem4dom  6707  php5dom  6708  phpm  6710  phplem4on  6712  dif1en  6724  dif1enen  6725  fisbth  6728  fin0  6730  fin0or  6731  fientri3  6754  unsnfidcex  6759  unsnfidcel  6760  fiintim  6768  fisseneq  6771  f1ofi  6781  endjusym  6931  eninl  6932  eninr  6933  pm54.43  6993  djuen  7012  dju1en  7014  djuassen  7018  xpdjuen  7019  uzenom  10085  hashennnuni  10412  hashennn  10413  hashcl  10414  hashfz1  10416  hashen  10417  fihashfn  10433  fihashdom  10436  hashunlem  10437  zfz1iso  10471  summodclem2  11037  zsumdc  11039  ennnfonelemen  11773  exmidunben  11778  ctinfom  11780  ctinf  11782  pwf1oexmid  12877  sbthom  12902