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

Proof

Step	Hyp	Ref	Expression
1		reuf1odnf.f	$$⊢\phi \to F:C\underset{1-1\; onto}{⟶}B$$
2		reuf1odnf.x	$$⊢\left(\phi \wedge x=F\left(y\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
3		reuf1odnf.z	$$⊢x=z\to \left(\psi \leftrightarrow \theta \right)$$
4		reuf1odnf.n	$$⊢Ⅎx\chi$$
5		f1of	$$⊢F:C\underset{1-1\; onto}{⟶}B\to F:C⟶B$$
6	1 5	syl	$$⊢\phi \to F:C⟶B$$
7	6	ffvelrnda	$$⊢\left(\phi \wedge y\in C\right)\to F\left(y\right)\in B$$
8		f1ofveu	$$⊢\left(F:C\underset{1-1\; onto}{⟶}B\wedge x\in B\right)\to \exists !y\in CF\left(y\right)=x$$
9		eqcom	$$⊢x=F\left(y\right)\leftrightarrow F\left(y\right)=x$$
10	9	reubii	$$⊢\exists !y\in Cx=F\left(y\right)\leftrightarrow \exists !y\in CF\left(y\right)=x$$
11	8 10	sylibr	$$⊢\left(F:C\underset{1-1\; onto}{⟶}B\wedge x\in B\right)\to \exists !y\in Cx=F\left(y\right)$$
12	1 11	sylan	$$⊢\left(\phi \wedge x\in B\right)\to \exists !y\in Cx=F\left(y\right)$$
13		sbceq1a	$$⊢x=F\left(y\right)\to \left(\psi \leftrightarrow \underset{\dot{}}{[}F\left(y\right)/x\underset{\dot{}}{]}\psi \right)$$
14	13	adantl	$$⊢\left(\phi \wedge x=F\left(y\right)\right)\to \left(\psi \leftrightarrow \underset{\dot{}}{[}F\left(y\right)/x\underset{\dot{}}{]}\psi \right)$$
15	3	cbvsbcvw	$$⊢\underset{\dot{}}{[}F\left(y\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}F\left(y\right)/z\underset{\dot{}}{]}\theta$$
16	14 15	bitrdi	$$⊢\left(\phi \wedge x=F\left(y\right)\right)\to \left(\psi \leftrightarrow \underset{\dot{}}{[}F\left(y\right)/z\underset{\dot{}}{]}\theta \right)$$
17	7 12 16	reuxfr1d	$$⊢\phi \to \left(\exists !x\in B\psi \leftrightarrow \exists !y\in C\underset{\dot{}}{[}F\left(y\right)/z\underset{\dot{}}{]}\theta \right)$$
18	15	a1i	$$⊢\phi \to \left(\underset{\dot{}}{[}F\left(y\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}F\left(y\right)/z\underset{\dot{}}{]}\theta \right)$$
19	18	bicomd	$$⊢\phi \to \left(\underset{\dot{}}{[}F\left(y\right)/z\underset{\dot{}}{]}\theta \leftrightarrow \underset{\dot{}}{[}F\left(y\right)/x\underset{\dot{}}{]}\psi \right)$$
20	19	reubidv	$$⊢\phi \to \left(\exists !y\in C\underset{\dot{}}{[}F\left(y\right)/z\underset{\dot{}}{]}\theta \leftrightarrow \exists !y\in C\underset{\dot{}}{[}F\left(y\right)/x\underset{\dot{}}{]}\psi \right)$$
21		fvexd	$$⊢\phi \to F\left(y\right)\in \mathrm{V}$$
22		nfv	$$⊢Ⅎx\phi$$
23	4	a1i	$$⊢\phi \to Ⅎx\chi$$
24	21 2 22 23	sbciedf	$$⊢\phi \to \left(\underset{\dot{}}{[}F\left(y\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
25	24	reubidv	$$⊢\phi \to \left(\exists !y\in C\underset{\dot{}}{[}F\left(y\right)/x\underset{\dot{}}{]}\psi \leftrightarrow \exists !y\in C\chi \right)$$
26	17 20 25	3bitrd	$$⊢\phi \to \left(\exists !x\in B\psi \leftrightarrow \exists !y\in C\chi \right)$$