![]() |
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 8156. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
ensymd.1 | ⊢ (𝜑 → 𝐴 ≈ 𝐵) |
Ref | Expression |
---|---|
ensymd | ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ensymd.1 | . 2 ⊢ (𝜑 → 𝐴 ≈ 𝐵) | |
2 | ensym 8156 | . 2 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐵 ≈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 class class class wbr 4786 ≈ cen 8104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7094 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-id 5157 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-fun 6031 df-fn 6032 df-f 6033 df-f1 6034 df-fo 6035 df-f1o 6036 df-er 7894 df-en 8108 |
This theorem is referenced by: f1imaeng 8167 f1imaen2g 8168 en2sn 8191 xpdom3 8212 omxpen 8216 mapdom2 8285 mapdom3 8286 limensuci 8290 phplem4 8296 php 8298 unxpdom2 8322 sucxpdom 8323 fiint 8391 marypha1lem 8493 infdifsn 8716 cnfcom2lem 8760 cardidm 8983 cardnueq0 8988 carden2a 8990 card1 8992 cardsdomel 8998 isinffi 9016 en2eqpr 9028 infxpenlem 9034 infxpidm2 9038 alephnbtwn2 9093 alephsucdom 9100 mappwen 9133 finnisoeu 9134 cdaen 9195 cda1en 9197 cdaassen 9204 xpcdaen 9205 infcda1 9215 pwcda1 9216 onacda 9219 cardacda 9220 cdanum 9221 ficardun 9224 pwsdompw 9226 infdif2 9232 infxp 9237 ackbij1lem5 9246 cfss 9287 ominf4 9334 isfin4-3 9337 fin23lem27 9350 alephsuc3 9602 canthp1lem1 9674 gchcda1 9678 gchinf 9679 pwfseqlem5 9685 pwcdandom 9689 gchcdaidm 9690 gchxpidm 9691 gchhar 9701 inttsk 9796 tskcard 9803 r1tskina 9804 tskuni 9805 hashkf 13316 fz1isolem 13440 isercolllem2 14597 summolem2a 14647 summolem2 14648 zsum 14650 prodmolem2a 14864 prodmolem2 14865 zprod 14867 4sqlem11 15859 mreexexd 16509 orbsta2 17947 psgnunilem1 18113 frlmisfrlm 20397 frlmiscvec 20398 ovoliunlem1 23483 rabfodom 29675 padct 29830 lindsdom 33729 matunitlindflem2 33732 heicant 33770 mblfinlem1 33772 eldioph2lem1 37842 isnumbasgrplem3 38194 fiuneneq 38294 enrelmap 38810 enmappw 38812 |
Copyright terms: Public domain | W3C validator |