Metamath Proof Explorer


Theorem domen2

Description: Equality-like theorem for equinumerosity and dominance. (Contributed by NM, 8-Nov-2003)

Ref Expression
Assertion domen2 ( 𝐴𝐵 → ( 𝐶𝐴𝐶𝐵 ) )

Proof

Step Hyp Ref Expression
1 domentr ( ( 𝐶𝐴𝐴𝐵 ) → 𝐶𝐵 )
2 1 ancoms ( ( 𝐴𝐵𝐶𝐴 ) → 𝐶𝐵 )
3 ensym ( 𝐴𝐵𝐵𝐴 )
4 domentr ( ( 𝐶𝐵𝐵𝐴 ) → 𝐶𝐴 )
5 4 ancoms ( ( 𝐵𝐴𝐶𝐵 ) → 𝐶𝐴 )
6 3 5 sylan ( ( 𝐴𝐵𝐶𝐵 ) → 𝐶𝐴 )
7 2 6 impbida ( 𝐴𝐵 → ( 𝐶𝐴𝐶𝐵 ) )