Theorem reuf1odnf

Description: There is exactly one element in each of two isomorphic sets. Variant of reuf1od with no distinct variable condition for ch . (Contributed by AV, 19-Mar-2023)

	Ref	Expression
Hypotheses	reuf1odnf.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐵 )
	reuf1odnf.x	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜓 ↔ 𝜒 ) )
	reuf1odnf.z	⊢ ( 𝑥 = 𝑧 → ( 𝜓 ↔ 𝜃 ) )
	reuf1odnf.n	⊢ Ⅎ 𝑥 𝜒
Assertion	reuf1odnf	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		reuf1odnf.f	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐵 )
2		reuf1odnf.x	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜓 ↔ 𝜒 ) )
3		reuf1odnf.z	⊢ ( 𝑥 = 𝑧 → ( 𝜓 ↔ 𝜃 ) )
4		reuf1odnf.n	⊢ Ⅎ 𝑥 𝜒
5		f1of	⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐵 → 𝐹 : 𝐶 ⟶ 𝐵 )
6	1 5	syl	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
7	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
8		f1ofveu	⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 ( 𝐹 ‘ 𝑦 ) = 𝑥 )
9		eqcom	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = 𝑥 )
10	9	reubii	⊢ ( ∃! 𝑦 ∈ 𝐶 𝑥 = ( 𝐹 ‘ 𝑦 ) ↔ ∃! 𝑦 ∈ 𝐶 ( 𝐹 ‘ 𝑦 ) = 𝑥 )
11	8 10	sylibr	⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = ( 𝐹 ‘ 𝑦 ) )
12	1 11	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = ( 𝐹 ‘ 𝑦 ) )
13		sbceq1a	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝜓 ↔ [ ( 𝐹 ‘ 𝑦 ) / 𝑥 ] 𝜓 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜓 ↔ [ ( 𝐹 ‘ 𝑦 ) / 𝑥 ] 𝜓 ) )
15	3	cbvsbcvw	⊢ ( [ ( 𝐹 ‘ 𝑦 ) / 𝑥 ] 𝜓 ↔ [ ( 𝐹 ‘ 𝑦 ) / 𝑧 ] 𝜃 )
16	14 15	bitrdi	⊢ ( ( 𝜑 ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → ( 𝜓 ↔ [ ( 𝐹 ‘ 𝑦 ) / 𝑧 ] 𝜃 ) )
17	7 12 16	reuxfr1d	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 [ ( 𝐹 ‘ 𝑦 ) / 𝑧 ] 𝜃 ) )
18	15	a1i	⊢ ( 𝜑 → ( [ ( 𝐹 ‘ 𝑦 ) / 𝑥 ] 𝜓 ↔ [ ( 𝐹 ‘ 𝑦 ) / 𝑧 ] 𝜃 ) )
19	18	bicomd	⊢ ( 𝜑 → ( [ ( 𝐹 ‘ 𝑦 ) / 𝑧 ] 𝜃 ↔ [ ( 𝐹 ‘ 𝑦 ) / 𝑥 ] 𝜓 ) )
20	19	reubidv	⊢ ( 𝜑 → ( ∃! 𝑦 ∈ 𝐶 [ ( 𝐹 ‘ 𝑦 ) / 𝑧 ] 𝜃 ↔ ∃! 𝑦 ∈ 𝐶 [ ( 𝐹 ‘ 𝑦 ) / 𝑥 ] 𝜓 ) )
21		fvexd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑦 ) ∈ V )
22		nfv	⊢ Ⅎ 𝑥 𝜑
23	4	a1i	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
24	21 2 22 23	sbciedf	⊢ ( 𝜑 → ( [ ( 𝐹 ‘ 𝑦 ) / 𝑥 ] 𝜓 ↔ 𝜒 ) )
25	24	reubidv	⊢ ( 𝜑 → ( ∃! 𝑦 ∈ 𝐶 [ ( 𝐹 ‘ 𝑦 ) / 𝑥 ] 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )
26	17 20 25	3bitrd	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )