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 8546. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ensymd.1 | ⊢ (𝜑 → 𝐴 ≈ 𝐵) |
Ref | Expression |
---|---|
ensymd | ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ensymd.1 | . 2 ⊢ (𝜑 → 𝐴 ≈ 𝐵) | |
2 | ensym 8546 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 class class class wbr 5057 ≈ cen 8494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-pw 4537 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-er 8278 df-en 8498 |
This theorem is referenced by: f1imaeng 8557 f1imaen2g 8558 en2sn 8581 xpdom3 8603 omxpen 8607 mapdom2 8676 mapdom3 8677 limensuci 8681 phplem4 8687 php 8689 unxpdom2 8714 sucxpdom 8715 fiint 8783 marypha1lem 8885 infdifsn 9108 cnfcom2lem 9152 cardidm 9376 cardnueq0 9381 carden2a 9383 card1 9385 cardsdomel 9391 isinffi 9409 en2eqpr 9421 infxpenlem 9427 infxpidm2 9431 alephnbtwn2 9486 alephsucdom 9493 mappwen 9526 finnisoeu 9527 djuen 9583 dju1en 9585 djuassen 9592 xpdjuen 9593 infdju1 9603 pwdju1 9604 onadju 9607 cardadju 9608 djunum 9609 ficardun 9612 pwsdompw 9614 infdif2 9620 infxp 9625 ackbij1lem5 9634 cfss 9675 ominf4 9722 isfin4p1 9725 fin23lem27 9738 alephsuc3 9990 canthp1lem1 10062 canthp1lem2 10063 gchdju1 10066 gchinf 10067 pwfseqlem5 10073 pwdjundom 10077 gchdjuidm 10078 gchxpidm 10079 gchhar 10089 inttsk 10184 tskcard 10191 r1tskina 10192 tskuni 10193 hashkf 13680 fz1isolem 13807 isercolllem2 15010 summolem2 15061 zsum 15063 prodmolem2 15277 zprod 15279 4sqlem11 16279 mreexexd 16907 psgnunilem1 18550 simpgnsgd 19151 frlmisfrlm 20920 frlmiscvec 20921 ovoliunlem1 24030 rabfodom 30193 unidifsnel 30222 unidifsnne 30223 fnpreimac 30344 padct 30381 lindsdom 34767 matunitlindflem2 34770 heicant 34808 mblfinlem1 34810 eldioph2lem1 39235 isnumbasgrplem3 39583 fiuneneq 39675 harval3 39782 enrelmap 40221 enmappw 40223 |
Copyright terms: Public domain | W3C validator |