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	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐵 )
	reuf1od.x	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	reuf1od	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		reuf1od.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐵 )
2		reuf1od.x	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜓 ↔ 𝜒 ) )
3		f1of	⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐵 → 𝐹 : 𝐶 ⟶ 𝐵 )
4	1 3	syl	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
5	4	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
6		f1ofveu	⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 ( 𝐹 ‘ 𝑦 ) = 𝑥 )
7		eqcom	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = 𝑥 )
8	7	reubii	⊢ ( ∃! 𝑦 ∈ 𝐶 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ∃! 𝑦 ∈ 𝐶 ( 𝐹 ‘ 𝑦 ) = 𝑥 )
9	6 8	sylibr	⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = ( 𝐹 ‘ 𝑦 ) )
10	1 9	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = ( 𝐹 ‘ 𝑦 ) )
11	5 10 2	reuxfr1d	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )