Metamath Proof Explorer


Theorem funcnv3

Description: A condition showing a class is single-rooted. (See funcnv ). (Contributed by NM, 26-May-2006)

Ref Expression
Assertion funcnv3 FunA-1yranA∃!xdomAxAy

Proof

Step Hyp Ref Expression
1 dfrn2 ranA=y|xxAy
2 1 abeq2i yranAxxAy
3 2 biimpi yranAxxAy
4 3 biantrurd yranA*xxAyxxAy*xxAy
5 4 ralbiia yranA*xxAyyranAxxAy*xxAy
6 funcnv FunA-1yranA*xxAy
7 df-reu ∃!xdomAxAy∃!xxdomAxAy
8 vex xV
9 vex yV
10 8 9 breldm xAyxdomA
11 10 pm4.71ri xAyxdomAxAy
12 11 eubii ∃!xxAy∃!xxdomAxAy
13 df-eu ∃!xxAyxxAy*xxAy
14 7 12 13 3bitr2i ∃!xdomAxAyxxAy*xxAy
15 14 ralbii yranA∃!xdomAxAyyranAxxAy*xxAy
16 5 6 15 3bitr4i FunA-1yranA∃!xdomAxAy