Metamath Proof Explorer


Theorem rmoun

Description: "At most one" restricted existential quantifier for a union implies the same quantifier on both sets. (Contributed by Thierry Arnoux, 27-Nov-2023)

Ref Expression
Assertion rmoun * x A B φ * x A φ * x B φ

Proof

Step Hyp Ref Expression
1 mooran2 * x x A φ x B φ * x x A φ * x x B φ
2 df-rmo * x A B φ * x x A B φ
3 elun x A B x A x B
4 3 anbi1i x A B φ x A x B φ
5 andir x A x B φ x A φ x B φ
6 4 5 bitri x A B φ x A φ x B φ
7 6 mobii * x x A B φ * x x A φ x B φ
8 2 7 bitri * x A B φ * x x A φ x B φ
9 df-rmo * x A φ * x x A φ
10 df-rmo * x B φ * x x B φ
11 9 10 anbi12i * x A φ * x B φ * x x A φ * x x B φ
12 1 8 11 3imtr4i * x A B φ * x A φ * x B φ