This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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