Theorem reuf1od

Description: There is exactly one element in each of two isomorphic sets. (Contributed by AV, 19-Mar-2023)

	Ref	Expression
Hypotheses	reuf1od.f	|- ( ph -> F : C -1-1-onto-> B )
	reuf1od.x	|- ( ( ph /\ x = ( F ` y ) ) -> ( ps <-> ch ) )
Assertion	reuf1od	|- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )

Proof

Step	Hyp	Ref	Expression
1		reuf1od.f	|- ( ph -> F : C -1-1-onto-> B )
2		reuf1od.x	|- ( ( ph /\ x = ( F ` y ) ) -> ( ps <-> ch ) )
3		f1of	|- ( F : C -1-1-onto-> B -> F : C --> B )
4	1 3	syl	|- ( ph -> F : C --> B )
5	4	ffvelcdmda	|- ( ( ph /\ y e. C ) -> ( F ` y ) e. B )
6		f1ofveu	|- ( ( F : C -1-1-onto-> B /\ x e. B ) -> E! y e. C ( F ` y ) = x )
7		eqcom	|- ( x = ( F ` y ) <-> ( F ` y ) = x )
8	7	reubii	|- ( E! y e. C x = ( F ` y ) <-> E! y e. C ( F ` y ) = x )
9	6 8	sylibr	|- ( ( F : C -1-1-onto-> B /\ x e. B ) -> E! y e. C x = ( F ` y ) )
10	1 9	sylan	|- ( ( ph /\ x e. B ) -> E! y e. C x = ( F ` y ) )
11	5 10 2	reuxfr1d	|- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )