Metamath Proof Explorer


Theorem rmoxfrd

Description: Transfer "at most one" restricted quantification from a variable x to another variable y contained in expression A . (Contributed by Thierry Arnoux, 7-Apr-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmoxfrd.1 φyCAB
rmoxfrd.2 φxB∃!yCx=A
rmoxfrd.3 φx=Aψχ
Assertion rmoxfrd φ*xBψ*yCχ

Proof

Step Hyp Ref Expression
1 rmoxfrd.1 φyCAB
2 rmoxfrd.2 φxB∃!yCx=A
3 rmoxfrd.3 φx=Aψχ
4 reurex ∃!yCx=AyCx=A
5 2 4 syl φxByCx=A
6 1 5 3 rexxfrd φxBψyCχ
7 df-rex xBψxxBψ
8 df-rex yCχyyCχ
9 6 7 8 3bitr3g φxxBψyyCχ
10 1 2 3 reuxfr1d φ∃!xBψ∃!yCχ
11 df-reu ∃!xBψ∃!xxBψ
12 df-reu ∃!yCχ∃!yyCχ
13 10 11 12 3bitr3g φ∃!xxBψ∃!yyCχ
14 9 13 imbi12d φxxBψ∃!xxBψyyCχ∃!yyCχ
15 moeu *xxBψxxBψ∃!xxBψ
16 moeu *yyCχyyCχ∃!yyCχ
17 14 15 16 3bitr4g φ*xxBψ*yyCχ
18 df-rmo *xBψ*xxBψ
19 df-rmo *yCχ*yyCχ
20 17 18 19 3bitr4g φ*xBψ*yCχ