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 8547. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ensymd.1 | ⊢ (𝜑 → 𝐴 ≈ 𝐵) |
Ref | Expression |
---|---|
ensymd | ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ensymd.1 | . 2 ⊢ (𝜑 → 𝐴 ≈ 𝐵) | |
2 | ensym 8547 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 class class class wbr 5058 ≈ cen 8495 |
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 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 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 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-er 8279 df-en 8499 |
This theorem is referenced by: f1imaeng 8558 f1imaen2g 8559 en2sn 8582 xpdom3 8604 omxpen 8608 mapdom2 8677 mapdom3 8678 limensuci 8682 phplem4 8688 php 8690 unxpdom2 8715 sucxpdom 8716 fiint 8784 marypha1lem 8886 infdifsn 9109 cnfcom2lem 9153 cardidm 9377 cardnueq0 9382 carden2a 9384 card1 9386 cardsdomel 9392 isinffi 9410 en2eqpr 9422 infxpenlem 9428 infxpidm2 9432 alephnbtwn2 9487 alephsucdom 9494 mappwen 9527 finnisoeu 9528 djuen 9584 dju1en 9586 djuassen 9593 xpdjuen 9594 infdju1 9604 pwdju1 9605 onadju 9608 cardadju 9609 djunum 9610 ficardun 9613 pwsdompw 9615 infdif2 9621 infxp 9626 ackbij1lem5 9635 cfss 9676 ominf4 9723 isfin4p1 9726 fin23lem27 9739 alephsuc3 9991 canthp1lem1 10063 canthp1lem2 10064 gchdju1 10067 gchinf 10068 pwfseqlem5 10074 pwdjundom 10078 gchdjuidm 10079 gchxpidm 10080 gchhar 10090 inttsk 10185 tskcard 10192 r1tskina 10193 tskuni 10194 hashkf 13682 fz1isolem 13809 isercolllem2 15012 summolem2 15063 zsum 15065 prodmolem2 15279 zprod 15281 4sqlem11 16281 mreexexd 16909 psgnunilem1 18552 simpgnsgd 19153 frlmisfrlm 20922 frlmiscvec 20923 ovoliunlem1 24032 rabfodom 30194 unidifsnel 30223 unidifsnne 30224 fnpreimac 30345 padct 30382 lindsdom 34768 matunitlindflem2 34771 heicant 34809 mblfinlem1 34811 eldioph2lem1 39237 isnumbasgrplem3 39585 fiuneneq 39677 harval3 39784 enrelmap 40223 enmappw 40225 |
Copyright terms: Public domain | W3C validator |