![]() |
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 8995. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ensymd.1 | ⊢ (𝜑 → 𝐴 ≈ 𝐵) |
Ref | Expression |
---|---|
ensymd | ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ensymd.1 | . 2 ⊢ (𝜑 → 𝐴 ≈ 𝐵) | |
2 | ensym 8995 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 class class class wbr 5147 ≈ cen 8932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7720 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-er 8699 df-en 8936 |
This theorem is referenced by: f1imaeng 9006 f1imaen2g 9007 en2snOLDOLD 9039 xpdom3 9066 omxpen 9070 mapdom2 9144 mapdom3 9145 limensuci 9149 phplem4OLD 9216 phpOLD 9218 unxpdom2 9250 sucxpdom 9251 fiint 9320 marypha1lem 9424 infdifsn 9648 cnfcom2lem 9692 cardidm 9950 cardnueq0 9955 carden2a 9957 card1 9959 cardsdomel 9965 isinffi 9983 en2eqpr 9998 infxpenlem 10004 infxpidm2 10008 alephnbtwn2 10063 alephsucdom 10070 mappwen 10103 finnisoeu 10104 djuen 10160 dju1en 10162 djuassen 10169 xpdjuen 10170 infdju1 10180 pwdju1 10181 onadju 10184 cardadju 10185 djunum 10186 nnadju 10188 ficardadju 10190 ficardun 10191 ficardunOLD 10192 pwsdompw 10195 infdif2 10201 infxp 10206 ackbij1lem5 10215 cfss 10256 ominf4 10303 isfin4p1 10306 fin23lem27 10319 alephsuc3 10571 canthp1lem1 10643 canthp1lem2 10644 gchdju1 10647 gchinf 10648 pwfseqlem5 10654 pwdjundom 10658 gchdjuidm 10659 gchxpidm 10660 gchhar 10670 inttsk 10765 tskcard 10772 r1tskina 10773 tskuni 10774 hashkf 14288 fz1isolem 14418 isercolllem2 15608 summolem2 15658 zsum 15660 prodmolem2 15875 zprod 15877 4sqlem11 16884 mreexexd 17588 psgnunilem1 19354 simpgnsgd 19962 frlmisfrlm 21387 frlmiscvec 21388 ovoliunlem1 25001 rabfodom 31721 unidifsnel 31750 unidifsnne 31751 fnpreimac 31874 padct 31922 lindsdom 36420 matunitlindflem2 36423 heicant 36461 mblfinlem1 36463 sticksstones18 40918 sticksstones19 40919 eldioph2lem1 41431 isnumbasgrplem3 41780 fiuneneq 41872 harval3 42222 enrelmap 42681 enmappw 42683 |
Copyright terms: Public domain | W3C validator |