ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ensymd Unicode version

Theorem ensymd 6353
Description: Symmetry of equinumerosity. Deduction form of ensym 6351. (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
StepHypRef Expression
1 ensymd.1 . 2  |-  ( ph  ->  A  ~~  B )
2 ensym 6351 . 2  |-  ( A 
~~  B  ->  B  ~~  A )
31, 2syl 14 1  |-  ( ph  ->  B  ~~  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   class class class wbr 3806    ~~ cen 6308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3917  ax-pow 3969  ax-pr 3993  ax-un 4217
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2613  df-un 2987  df-in 2989  df-ss 2996  df-pw 3403  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-br 3807  df-opab 3861  df-id 4077  df-xp 4398  df-rel 4399  df-cnv 4400  df-co 4401  df-dm 4402  df-rn 4403  df-res 4404  df-ima 4405  df-fun 4955  df-fn 4956  df-f 4957  df-f1 4958  df-fo 4959  df-f1o 4960  df-er 6195  df-en 6311
This theorem is referenced by:  f1imaeng  6362  f1imaen2g  6363  en2sn  6381  xpdom3m  6401  phplem4  6413  phplem4dom  6420  php5dom  6421  phpm  6423  phplem4on  6425  dif1en  6437  dif1enen  6438  fisbth  6441  fin0  6443  fin0or  6444  fientri3  6461  unsnfidcex  6466  unsnfidcel  6467  fisseneq  6476  f1ofi  6485  pm54.43  6595  uzenom  9584  hashennnuni  9880  hashennn  9881  hashcl  9882  hashfz1  9884  hashen  9885  fihashfn  9901  fihashdom  9904  hashunlem  9905
  Copyright terms: Public domain W3C validator