Theorem domen1 7697

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

Assertion

Ref	Expression
domen1	|- ( A ~~ B -> ( A ~<_ C <-> B ~<_ C ) )

Proof of Theorem domen1

Step	Hyp	Ref	Expression
1		ensym 7602	. . 3 |- ( A ~~ B -> B ~~ A )
2		endomtr 7611	. . 3 |- ( ( B ~~ A /\ A ~<_ C ) -> B ~<_ C )
3	1, 2	sylan 469	. 2 |- ( ( A ~~ B /\ A ~<_ C ) -> B ~<_ C )
4		endomtr 7611	. 2 |- ( ( A ~~ B /\ B ~<_ C ) -> A ~<_ C )
5	3, 4	impbida 833	1 |- ( A ~~ B -> ( A ~<_ C <-> B ~<_ C ) )

Syntax hints:   -> wi 4   <-> wb 184   class class class wbr 4395   ~~ cen 7551   ~<_ cdom 7552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-er 7348  df-en 7555  df-dom 7556

This theorem is referenced by:  unxpwdom2  8048  carddomi2  8383  cdadom2  8599  cdainf  8604  cdalepw  8608  pwcdadom  8628  gchpwdom  9078  hargch  9081  dis2ndc  20253