Metamath Proof Explorer

Theorem rexor

Description: Alias for r19.43 for easier lookup. (Contributed by SN, 5-Jul-2025) (New usage is discouraged.)

Ref Expression
Assertion rexor 
|- ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) )

Proof

Step Hyp Ref Expression
1 r19.43 
 |-  ( E. x e. A ( ph \/ ps ) <-> ( E. x e. A ph \/ E. x e. A ps ) )