Metamath Proof Explorer

Theorem ralrnmpt

Description: A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker ralrnmptw when possible. (Contributed by Mario Carneiro, 20-Aug-2015) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ralrnmpt.1 
 |-  F = ( x e. A |-> B )
2 ralrnmpt.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 nfv 
 |-  F/ w ps
8 nfsbc1v 
 |-  F/ y [. w / y ]. ps
9 sbceq1a 
 |-  ( y = w -> ( ps <-> [. w / y ]. ps ) )
10 7 8 9 cbvral 
 |-  ( A. y e. ran F ps <-> A. w e. ran F [. w / y ]. ps )
11 10 bicomi 
 |-  ( A. w e. ran F [. w / y ]. ps <-> A. y e. ran F ps )
12 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
13 1 12 nfcxfr 
 |-  F/_ x F
14 nfcv 
 |-  F/_ x z
15 13 14 nffv 
 |-  F/_ x ( F ` z )
16 nfv 
 |-  F/ x ps
17 15 16 nfsbc 
 |-  F/ x [. ( F ` z ) / y ]. ps
18 nfv 
 |-  F/ z [. ( F ` x ) / y ]. ps
19 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
20 19 sbceq1d 
 |-  ( z = x -> ( [. ( F ` z ) / y ]. ps <-> [. ( F ` x ) / y ]. ps ) )
21 17 18 20 cbvral 
 |-  ( A. z e. A [. ( F ` z ) / y ]. ps <-> A. x e. A [. ( F ` x ) / y ]. ps )
22 6 11 21 3bitr3g 
 |-  ( A. x e. A B e. V -> ( A. y e. ran F ps <-> A. x e. A [. ( F ` x ) / y ]. ps ) )
23 1 fvmpt2 
 |-  ( ( x e. A /\ B e. V ) -> ( F ` x ) = B )
24 23 sbceq1d 
 |-  ( ( x e. A /\ B e. V ) -> ( [. ( F ` x ) / y ]. ps <-> [. B / y ]. ps ) )
25 2 sbcieg 
 |-  ( B e. V -> ( [. B / y ]. ps <-> ch ) )
26 25 adantl 
 |-  ( ( x e. A /\ B e. V ) -> ( [. B / y ]. ps <-> ch ) )
27 24 26 bitrd 
 |-  ( ( x e. A /\ B e. V ) -> ( [. ( F ` x ) / y ]. ps <-> ch ) )
28 27 ralimiaa 
 |-  ( A. x e. A B e. V -> A. x e. A ( [. ( F ` x ) / y ]. ps <-> ch ) )
29 ralbi 
 |-  ( A. x e. A ( [. ( F ` x ) / y ]. ps <-> ch ) -> ( A. x e. A [. ( F ` x ) / y ]. ps <-> A. x e. A ch ) )
30 28 29 syl 
 |-  ( A. x e. A B e. V -> ( A. x e. A [. ( F ` x ) / y ]. ps <-> A. x e. A ch ) )
31 22 30 bitrd 
 |-  ( A. x e. A B e. V -> ( A. y e. ran F ps <-> A. x e. A ch ) )