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	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}B$$
	reuf1od.x	$$⊢\left(\phi \wedge x=F\left(y\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	reuf1od	$$⊢\phi \to \left(\exists !x\in B\psi \leftrightarrow \exists !y\in C\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		reuf1od.f	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}B$$
2		reuf1od.x	$$⊢\left(\phi \wedge x=F\left(y\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
3		f1of	$$⊢F:C\underset{1-1\; onto}{⟶}B\to F:C⟶B$$
4	1 3	syl	$$⊢\phi \to F:C⟶B$$
5	4	ffvelcdmda	$$⊢\left(\phi \wedge y\in C\right)\to F\left(y\right)\in B$$
6		f1ofveu	$$⊢\left(F:C\underset{1-1\; onto}{⟶}B\wedge x\in B\right)\to \exists !y\in CF\left(y\right)=x$$
7		eqcom	$$⊢x=F\left(y\right)\leftrightarrow F\left(y\right)=x$$
8	7	reubii	$$⊢\exists !y\in Cx=F\left(y\right)\leftrightarrow \exists !y\in CF\left(y\right)=x$$
9	6 8	sylibr	$$⊢\left(F:C\underset{1-1\; onto}{⟶}B\wedge x\in B\right)\to \exists !y\in Cx=F\left(y\right)$$
10	1 9	sylan	$$⊢\left(\phi \wedge x\in B\right)\to \exists !y\in Cx=F\left(y\right)$$
11	5 10 2	reuxfr1d	$$⊢\phi \to \left(\exists !x\in B\psi \leftrightarrow \exists !y\in C\chi \right)$$