Metamath Proof Explorer

Theorem ralrnmptw

Description: A restricted quantifier over an image set. Version of ralrnmpt with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 20-Aug-2015) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Hypotheses ralrnmptw.1 
|- F = ( x e. A |-> B )
ralrnmptw.2 
|- ( y = B -> ( ps <-> ch ) )
Assertion ralrnmptw 
|- ( A. x e. A B e. V -> ( A. y e. ran F ps <-> A. x e. A ch ) )

Proof

Step Hyp Ref Expression
1 ralrnmptw.1 
 |-  F = ( x e. A |-> B )
2 ralrnmptw.2 
 |-  ( y = B -> ( ps <-> ch ) )
3 1 fnmpt 
 |-  ( A. x e. A B e. V -> F Fn A )
4 dfsbcq 
 |-  ( w = ( F ` z ) -> ( [. w / y ]. ps <-> [. ( F ` z ) / y ]. ps ) )
5 4 ralrn 
 |-  ( F Fn A -> ( A. w e. ran F [. w / y ]. ps <-> A. z e. A [. ( F ` z ) / y ]. ps ) )
6 3 5 syl 
 |-  ( A. x e. A B e. V -> ( A. w e. ran F [. w / y ]. ps <-> A. z e. A [. ( F ` z ) / y ]. ps ) )
7 nfsbc1v 
 |-  F/ y [. w / y ]. ps
8 nfv 
 |-  F/ w ps
9 sbceq2a 
 |-  ( w = y -> ( [. w / y ]. ps <-> ps ) )
10 7 8 9 cbvralw 
 |-  ( A. w e. ran F [. w / y ]. ps <-> A. y e. ran F ps )
11 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
12 1 11 nfcxfr 
 |-  F/_ x F
13 nfcv 
 |-  F/_ x z
14 12 13 nffv 
 |-  F/_ x ( F ` z )
15 nfv 
 |-  F/ x ps
16 14 15 nfsbcw 
 |-  F/ x [. ( F ` z ) / y ]. ps
17 nfv 
 |-  F/ z [. ( F ` x ) / y ]. ps
18 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
19 18 sbceq1d 
 |-  ( z = x -> ( [. ( F ` z ) / y ]. ps <-> [. ( F ` x ) / y ]. ps ) )
20 16 17 19 cbvralw 
 |-  ( A. z e. A [. ( F ` z ) / y ]. ps <-> A. x e. A [. ( F ` x ) / y ]. ps )
21 6 10 20 3bitr3g 
 |-  ( A. x e. A B e. V -> ( A. y e. ran F ps <-> A. x e. A [. ( F ` x ) / y ]. ps ) )
22 1 fvmpt2 
 |-  ( ( x e. A /\ B e. V ) -> ( F ` x ) = B )
23 22 sbceq1d 
 |-  ( ( x e. A /\ B e. V ) -> ( [. ( F ` x ) / y ]. ps <-> [. B / y ]. ps ) )
24 2 sbcieg 
 |-  ( B e. V -> ( [. B / y ]. ps <-> ch ) )
25 24 adantl 
 |-  ( ( x e. A /\ B e. V ) -> ( [. B / y ]. ps <-> ch ) )
26 23 25 bitrd 
 |-  ( ( x e. A /\ B e. V ) -> ( [. ( F ` x ) / y ]. ps <-> ch ) )
27 26 ralimiaa 
 |-  ( A. x e. A B e. V -> A. x e. A ( [. ( F ` x ) / y ]. ps <-> ch ) )
28 ralbi 
 |-  ( A. x e. A ( [. ( F ` x ) / y ]. ps <-> ch ) -> ( A. x e. A [. ( F ` x ) / y ]. ps <-> A. x e. A ch ) )
29 27 28 syl 
 |-  ( A. x e. A B e. V -> ( A. x e. A [. ( F ` x ) / y ]. ps <-> A. x e. A ch ) )
30 21 29 bitrd 
 |-  ( A. x e. A B e. V -> ( A. y e. ran F ps <-> A. x e. A ch ) )