Metamath Proof Explorer


Theorem raleleqOLD

Description: Obsolete version of raleleq as of 18-Jul-2025. (Contributed by AV, 30-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion raleleqOLD A = B x A x B

Proof

Step Hyp Ref Expression
1 ralel x B x B
2 id A = B A = B
3 2 raleqdv A = B x A x B x B x B
4 1 3 mpbiri A = B x A x B