Metamath Proof Explorer


Theorem reuxfr1d

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Cf. reuxfr1ds . (Contributed by Thierry Arnoux, 7-Apr-2017)

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

Proof

Step Hyp Ref Expression
1 reuxfr1d.1 φyCAB
2 reuxfr1d.2 φxB∃!yCx=A
3 reuxfr1d.3 φx=Aψχ
4 reurex ∃!yCx=AyCx=A
5 2 4 syl φxByCx=A
6 5 biantrurd φxBψyCx=Aψ
7 r19.41v yCx=AψyCx=Aψ
8 3 pm5.32da φx=Aψx=Aχ
9 8 rexbidv φyCx=AψyCx=Aχ
10 7 9 bitr3id φyCx=AψyCx=Aχ
11 10 adantr φxByCx=AψyCx=Aχ
12 6 11 bitrd φxBψyCx=Aχ
13 12 reubidva φ∃!xBψ∃!xByCx=Aχ
14 reurmo ∃!yCx=A*yCx=A
15 2 14 syl φxB*yCx=A
16 1 15 reuxfrd φ∃!xByCx=Aχ∃!yCχ
17 13 16 bitrd φ∃!xBψ∃!yCχ