Metamath Proof Explorer


Theorem raleq

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995) Remove usage of ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 30-Apr-2023) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025)

Ref Expression
Assertion raleq A = B x A φ x B φ

Proof

Step Hyp Ref Expression
1 rexeq A = B x A ¬ φ x B ¬ φ
2 rexnal x A ¬ φ ¬ x A φ
3 rexnal x B ¬ φ ¬ x B φ
4 1 2 3 3bitr3g A = B ¬ x A φ ¬ x B φ
5 4 con4bid A = B x A φ x B φ