Metamath Proof Explorer


Theorem raleleqOLD

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

Ref Expression
Assertion raleleqOLD
|- ( A = B -> A. x e. A x e. B )

Proof

Step Hyp Ref Expression
1 eleq2
 |-  ( A = B -> ( x e. A <-> x e. B ) )
2 1 biimpd
 |-  ( A = B -> ( x e. A -> x e. B ) )
3 2 ralrimiv
 |-  ( A = B -> A. x e. A x e. B )