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=xAB
ralrnmpt.2 y=Bψχ
Assertion ralrnmpt xABVyranFψxAχ

Proof

Step Hyp Ref Expression
1 ralrnmpt.1 F=xAB
2 ralrnmpt.2 y=Bψχ
3 1 fnmpt xABVFFnA
4 dfsbcq w=Fz[˙w/y]˙ψ[˙Fz/y]˙ψ
5 4 ralrn FFnAwranF[˙w/y]˙ψzA[˙Fz/y]˙ψ
6 3 5 syl xABVwranF[˙w/y]˙ψzA[˙Fz/y]˙ψ
7 nfv wψ
8 nfsbc1v y[˙w/y]˙ψ
9 sbceq1a y=wψ[˙w/y]˙ψ
10 7 8 9 cbvral yranFψwranF[˙w/y]˙ψ
11 10 bicomi wranF[˙w/y]˙ψyranFψ
12 nfmpt1 _xxAB
13 1 12 nfcxfr _xF
14 nfcv _xz
15 13 14 nffv _xFz
16 nfv xψ
17 15 16 nfsbc x[˙Fz/y]˙ψ
18 nfv z[˙Fx/y]˙ψ
19 fveq2 z=xFz=Fx
20 19 sbceq1d z=x[˙Fz/y]˙ψ[˙Fx/y]˙ψ
21 17 18 20 cbvral zA[˙Fz/y]˙ψxA[˙Fx/y]˙ψ
22 6 11 21 3bitr3g xABVyranFψxA[˙Fx/y]˙ψ
23 1 fvmpt2 xABVFx=B
24 23 sbceq1d xABV[˙Fx/y]˙ψ[˙B/y]˙ψ
25 2 sbcieg BV[˙B/y]˙ψχ
26 25 adantl xABV[˙B/y]˙ψχ
27 24 26 bitrd xABV[˙Fx/y]˙ψχ
28 27 ralimiaa xABVxA[˙Fx/y]˙ψχ
29 ralbi xA[˙Fx/y]˙ψχxA[˙Fx/y]˙ψxAχ
30 28 29 syl xABVxA[˙Fx/y]˙ψxAχ
31 22 30 bitrd xABVyranFψxAχ