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 ) ) )