Metamath Proof Explorer

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 
|- ( ph -> F : C -1-1-onto-> B )
reuf1odnf.x 
|- ( ( ph /\ x = ( F ` y ) ) -> ( ps <-> ch ) )
reuf1odnf.z 
|- ( x = z -> ( ps <-> th ) )
reuf1odnf.n 
|- F/ x ch
Assertion reuf1odnf 
|- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )

Proof

Step Hyp Ref Expression
1 reuf1odnf.f 
 |-  ( ph -> F : C -1-1-onto-> B )
2 reuf1odnf.x 
 |-  ( ( ph /\ x = ( F ` y ) ) -> ( ps <-> ch ) )
3 reuf1odnf.z 
 |-  ( x = z -> ( ps <-> th ) )
4 reuf1odnf.n 
 |-  F/ x ch
5 f1of 
 |-  ( F : C -1-1-onto-> B -> F : C --> B )
6 1 5 syl 
 |-  ( ph -> F : C --> B )
7 6 ffvelrnda 
 |-  ( ( ph /\ y e. C ) -> ( F ` y ) e. B )
8 f1ofveu 
 |-  ( ( F : C -1-1-onto-> B /\ x e. B ) -> E! y e. C ( F ` y ) = x )
9 eqcom 
 |-  ( x = ( F ` y ) <-> ( F ` y ) = x )
10 9 reubii 
 |-  ( E! y e. C x = ( F ` y ) <-> E! y e. C ( F ` y ) = x )
11 8 10 sylibr 
 |-  ( ( F : C -1-1-onto-> B /\ x e. B ) -> E! y e. C x = ( F ` y ) )
12 1 11 sylan 
 |-  ( ( ph /\ x e. B ) -> E! y e. C x = ( F ` y ) )
13 sbceq1a 
 |-  ( x = ( F ` y ) -> ( ps <-> [. ( F ` y ) / x ]. ps ) )
14 13 adantl 
 |-  ( ( ph /\ x = ( F ` y ) ) -> ( ps <-> [. ( F ` y ) / x ]. ps ) )
15 3 cbvsbcvw 
 |-  ( [. ( F ` y ) / x ]. ps <-> [. ( F ` y ) / z ]. th )
16 14 15 bitrdi 
 |-  ( ( ph /\ x = ( F ` y ) ) -> ( ps <-> [. ( F ` y ) / z ]. th ) )
17 7 12 16 reuxfr1d 
 |-  ( ph -> ( E! x e. B ps <-> E! y e. C [. ( F ` y ) / z ]. th ) )
18 15 a1i 
 |-  ( ph -> ( [. ( F ` y ) / x ]. ps <-> [. ( F ` y ) / z ]. th ) )
19 18 bicomd 
 |-  ( ph -> ( [. ( F ` y ) / z ]. th <-> [. ( F ` y ) / x ]. ps ) )
20 19 reubidv 
 |-  ( ph -> ( E! y e. C [. ( F ` y ) / z ]. th <-> E! y e. C [. ( F ` y ) / x ]. ps ) )
21 fvexd 
 |-  ( ph -> ( F ` y ) e. _V )
22 nfv 
 |-  F/ x ph
23 4 a1i 
 |-  ( ph -> F/ x ch )
24 21 2 22 23 sbciedf 
 |-  ( ph -> ( [. ( F ` y ) / x ]. ps <-> ch ) )
25 24 reubidv 
 |-  ( ph -> ( E! y e. C [. ( F ` y ) / x ]. ps <-> E! y e. C ch ) )
26 17 20 25 3bitrd 
 |-  ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )