Metamath Proof Explorer


Theorem bnj1414

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1414.1 B=predXARypredXARtrClyAR
Assertion bnj1414 RFrSeAXAtrClXAR=B

Proof

Step Hyp Ref Expression
1 bnj1414.1 B=predXARypredXARtrClyAR
2 eqid predXARytrClXARtrClyAR=predXARytrClXARtrClyAR
3 biid RFrSeAXARFrSeAXA
4 biid BVTrFoBARpredXARBBVTrFoBARpredXARB
5 1 2 3 4 bnj1408 RFrSeAXAtrClXAR=B