Theorem elec1cnvxrn2

Description: Elementhood in the converse range Cartesian product coset of A . (Contributed by Peter Mazsa, 11-Jul-2021)

	Ref	Expression
Assertion	elec1cnvxrn2	|- ( B e. V -> ( B e. [ A ] `' ( R |X. S ) <-> E. y E. z ( A = <. y , z >. /\ B R y /\ B S z ) ) )

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' ( R |X. S )
2		relelec	|- ( Rel `' ( R |X. S ) -> ( B e. [ A ] `' ( R |X. S ) <-> A `' ( R |X. S ) B ) )
3	1 2	ax-mp	|- ( B e. [ A ] `' ( R |X. S ) <-> A `' ( R |X. S ) B )
4		br1cnvxrn2	|- ( B e. V -> ( A `' ( R |X. S ) B <-> E. y E. z ( A = <. y , z >. /\ B R y /\ B S z ) ) )
5	3 4	bitrid	|- ( B e. V -> ( B e. [ A ] `' ( R |X. S ) <-> E. y E. z ( A = <. y , z >. /\ B R y /\ B S z ) ) )