| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ensymd | Structured version Visualization version GIF version | ||
| Description: Symmetry of equinumerosity. Deduction form of ensym 8988. (Contributed by David Moews, 1-May-2017.) |
| Ref | Expression |
|---|---|
| ensymd.1 | ⊢ (𝜑 → 𝐴 ≈ 𝐵) |
| Ref | Expression |
|---|---|
| ensymd | ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ensymd.1 | . 2 ⊢ (𝜑 → 𝐴 ≈ 𝐵) | |
| 2 | ensym 8988 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
| 3 | 1, 2 | syl 18 | 1 ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 class class class wbr 5104 ≈ cen 8928 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5250 ax-pow 5326 ax-pr 5394 ax-un 7722 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5105 df-opab 5167 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-er 8682 df-en 8932 |
| This theorem is referenced by: f1imaeng 8999 f1imaen2g 9000 xpdom3 9051 omxpen 9055 mapdom2 9124 mapdom3 9125 limensuci 9129 unxpdom2 9208 sucxpdom 9209 marypha1lem 9381 infdifsn 9614 cnfcom2lem 9658 cardidm 9933 cardnueq0 9938 carden2a 9940 card1 9942 cardsdomel 9948 isinffi 9966 en2eqpr 9979 infxpenlem 9985 infxpidm2 9989 alephnbtwn2 10044 alephsucdom 10051 mappwen 10084 finnisoeu 10085 djuen 10141 dju1en 10143 djuassen 10150 xpdjuen 10151 infdju1 10161 pwdju1 10162 onadju 10165 cardadju 10166 djunum 10167 nnadju 10169 ficardadju 10171 ficardun 10172 pwsdompw 10174 infdif2 10180 infxp 10185 ackbij1lem5 10194 cfss 10237 ominf4 10284 isfin4p1 10287 fin23lem27 10300 alephsuc3 10553 canthp1lem1 10625 canthp1lem2 10626 gchdju1 10629 gchinf 10630 pwfseqlem5 10636 pwdjundom 10640 gchdjuidm 10641 gchxpidm 10642 gchhar 10652 inttsk 10747 tskcard 10754 r1tskina 10755 tskuni 10756 hashkf 14356 hashpss 14434 fz1isolem 14486 isercolllem2 15705 summolem2 15755 zsum 15757 prodmolem2 15977 zprod 15979 4sqlem11 17003 mreexexd 17692 psgnunilem1 19551 simpgnsgd 20160 frlmisfrlm 21955 frlmiscvec 21956 ovoliunlem1 25618 rabfodom 32757 unidifsnel 32787 unidifsnne 32788 fnpreimac 32923 hashimaf1 33063 1enumen 35395 lindsdom 38120 matunitlindflem2 38123 heicant 38161 mblfinlem1 38163 sticksstones18 42788 sticksstones19 42789 eldioph2lem1 43348 isnumbasgrplem3 43689 fiuneneq 43776 harval3 44121 enrelmap 44580 enmappw 44582 |
| Copyright terms: Public domain | W3C validator |