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 | |
|
ralrnmpt.2 | |
||
Assertion | ralrnmpt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrnmpt.1 | |
|
2 | ralrnmpt.2 | |
|
3 | 1 | fnmpt | |
4 | dfsbcq | |
|
5 | 4 | ralrn | |
6 | 3 5 | syl | |
7 | nfv | |
|
8 | nfsbc1v | |
|
9 | sbceq1a | |
|
10 | 7 8 9 | cbvral | |
11 | 10 | bicomi | |
12 | nfmpt1 | |
|
13 | 1 12 | nfcxfr | |
14 | nfcv | |
|
15 | 13 14 | nffv | |
16 | nfv | |
|
17 | 15 16 | nfsbc | |
18 | nfv | |
|
19 | fveq2 | |
|
20 | 19 | sbceq1d | |
21 | 17 18 20 | cbvral | |
22 | 6 11 21 | 3bitr3g | |
23 | 1 | fvmpt2 | |
24 | 23 | sbceq1d | |
25 | 2 | sbcieg | |
26 | 25 | adantl | |
27 | 24 26 | bitrd | |
28 | 27 | ralimiaa | |
29 | ralbi | |
|
30 | 28 29 | syl | |
31 | 22 30 | bitrd | |