Metamath Proof Explorer


Theorem rmoeq1

Description: Equality theorem for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023) Avoid ax-8 . (Revised by Wolf Lammen, 12-Mar-2025)

Ref Expression
Assertion rmoeq1 A = B * x A φ * x B φ

Proof

Step Hyp Ref Expression
1 dfcleq A = B x x A x B
2 1 biimpi A = B x x A x B
3 anbi1 x A x B x A φ x B φ
4 3 imbi1d x A x B x A φ x = z x B φ x = z
5 4 alimi x x A x B x x A φ x = z x B φ x = z
6 albi x x A φ x = z x B φ x = z x x A φ x = z x x B φ x = z
7 2 5 6 3syl A = B x x A φ x = z x x B φ x = z
8 7 exbidv A = B z x x A φ x = z z x x B φ x = z
9 df-mo * x x A φ z x x A φ x = z
10 df-mo * x x B φ z x x B φ x = z
11 8 9 10 3bitr4g A = B * x x A φ * x x B φ
12 df-rmo * x A φ * x x A φ
13 df-rmo * x B φ * x x B φ
14 11 12 13 3bitr4g A = B * x A φ * x B φ