Theorem ensymd 7023

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

Syntax hints:   -> wi 4   class class class wbr 4109   ~~ cen 6973

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-res 4761  df-ima 4762  df-fun 5354  df-fn 5355  df-f 5356  df-f1 5357  df-fo 5358  df-f1o 5359  df-er 6767  df-en 6976

This theorem is referenced by:  f1imaeng  7032  f1imaen2g  7033  en2sn  7055  xpdom3m  7085  phplem4  7109  phplem4dom  7116  php5dom  7117  phpm  7120  phplem4on  7122  dif1en  7136  dif1enen  7137  fisbth  7140  fin0  7142  fin0or  7143  fidcen  7156  fientri3  7175  unsnfidcex  7180  unsnfidcel  7181  fiintim  7191  fisseneq  7195  f1ofi  7210  fipwfi  7272  endjusym  7387  eninl  7388  eninr  7389  pm54.43  7487  djuen  7518  dju1en  7520  djuassen  7524  xpdjuen  7525  uzenom  10787  hashennnuni  11142  hashennn  11143  hashcl  11144  hashfz1  11146  hashen  11147  fihashfn  11164  fihashdom  11167  hashunlem  11168  sseqn  11203  zfz1iso  11213  summodclem2  12068  zsumdc  12070  prodmodclem2  12263  zproddc  12265  4sqlem11  13099  ennnfonelemen  13172  exmidunben  13177  ctinfom  13179  ctinf  13181  isnzr2  14329  znfi  14803  znhash  14804  usgrsizedgen  16208  upgr2wlkdc  16372  eupthfi  16446  pwf1oexmid  16773  nnnninfen  16799  sbthom  16806