Metamath Proof Explorer


Theorem moxfr

Description: Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015)

Ref Expression
Hypotheses moxfr.a A V
moxfr.b ∃! y x = A
moxfr.c x = A φ ψ
Assertion moxfr * x φ * y ψ

Proof

Step Hyp Ref Expression
1 moxfr.a A V
2 moxfr.b ∃! y x = A
3 moxfr.c x = A φ ψ
4 1 a1i y V A V
5 euex ∃! y x = A y x = A
6 2 5 ax-mp y x = A
7 rexv y V x = A y x = A
8 6 7 mpbir y V x = A
9 8 a1i x V y V x = A
10 4 9 3 rexxfr x V φ y V ψ
11 rexv x V φ x φ
12 rexv y V ψ y ψ
13 10 11 12 3bitr3i x φ y ψ
14 1 2 3 euxfrw ∃! x φ ∃! y ψ
15 13 14 imbi12i x φ ∃! x φ y ψ ∃! y ψ
16 moeu * x φ x φ ∃! x φ
17 moeu * y ψ y ψ ∃! y ψ
18 15 16 17 3bitr4i * x φ * y ψ