Metamath Proof Explorer

Theorem brinxprnres

Description: Binary relation on a restriction. (Contributed by Peter Mazsa, 2-Jan-2019)

		Ref	Expression
	Assertion	brinxprnres	\|- ( C e. V -> ( B ( R i^i ( A X. ran ( R \|` A ) ) ) C <-> ( B e. A /\ B R C ) ) )

Step	Hyp	Ref	Expression
1		brres2	\|- ( B ( R \|` A ) C <-> B ( R i^i ( A X. ran ( R \|` A ) ) ) C )
2		brres	\|- ( C e. V -> ( B ( R \|` A ) C <-> ( B e. A /\ B R C ) ) )
3	1 2	bitr3id	\|- ( C e. V -> ( B ( R i^i ( A X. ran ( R \|` A ) ) ) C <-> ( B e. A /\ B R C ) ) )

Step

Hyp

Ref

Expression

 |-  ( B ( R |` A ) C <-> B ( R i^i ( A X. ran ( R |` A ) ) ) C )

 |-  ( C e. V -> ( B ( R |` A ) C <-> ( B e. A /\ B R C ) ) )

1 2

 |-  ( C e. V -> ( B ( R i^i ( A X. ran ( R |` A ) ) ) C <-> ( B e. A /\ B R C ) ) )