Metamath Proof Explorer


Theorem reusv1

Description: Two ways to express single-valuedness of a class expression C ( y ) . (Contributed by NM, 16-Dec-2012) (Proof shortened by Mario Carneiro, 18-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

Ref Expression
Assertion reusv1
|- ( E. y e. B ph -> ( E! x e. A A. y e. B ( ph -> x = C ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )

Proof

Step Hyp Ref Expression
1 nfra1
 |-  F/ y A. y e. B ( ph -> x = C )
2 1 nfmov
 |-  F/ y E* x A. y e. B ( ph -> x = C )
3 rsp
 |-  ( A. y e. B ( ph -> x = C ) -> ( y e. B -> ( ph -> x = C ) ) )
4 3 com3l
 |-  ( y e. B -> ( ph -> ( A. y e. B ( ph -> x = C ) -> x = C ) ) )
5 4 alrimdv
 |-  ( y e. B -> ( ph -> A. x ( A. y e. B ( ph -> x = C ) -> x = C ) ) )
6 mo2icl
 |-  ( A. x ( A. y e. B ( ph -> x = C ) -> x = C ) -> E* x A. y e. B ( ph -> x = C ) )
7 5 6 syl6
 |-  ( y e. B -> ( ph -> E* x A. y e. B ( ph -> x = C ) ) )
8 2 7 rexlimi
 |-  ( E. y e. B ph -> E* x A. y e. B ( ph -> x = C ) )
9 mormo
 |-  ( E* x A. y e. B ( ph -> x = C ) -> E* x e. A A. y e. B ( ph -> x = C ) )
10 reu5
 |-  ( E! x e. A A. y e. B ( ph -> x = C ) <-> ( E. x e. A A. y e. B ( ph -> x = C ) /\ E* x e. A A. y e. B ( ph -> x = C ) ) )
11 10 rbaib
 |-  ( E* x e. A A. y e. B ( ph -> x = C ) -> ( E! x e. A A. y e. B ( ph -> x = C ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )
12 8 9 11 3syl
 |-  ( E. y e. B ph -> ( E! x e. A A. y e. B ( ph -> x = C ) <-> E. x e. A A. y e. B ( ph -> x = C ) ) )