Theorem fuco2el

Description: Equivalence of product functor. (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Assertion	fuco2el	|- ( <. <. K , L >. , <. F , G >. >. e. ( S X. R ) <-> ( K S L /\ F R G ) )

Proof

Step	Hyp	Ref	Expression
1		opelxp	|- ( <. <. K , L >. , <. F , G >. >. e. ( S X. R ) <-> ( <. K , L >. e. S /\ <. F , G >. e. R ) )
2		df-br	|- ( K S L <-> <. K , L >. e. S )
3		df-br	|- ( F R G <-> <. F , G >. e. R )
4	2 3	anbi12i	|- ( ( K S L /\ F R G ) <-> ( <. K , L >. e. S /\ <. F , G >. e. R ) )
5	1 4	bitr4i	|- ( <. <. K , L >. , <. F , G >. >. e. ( S X. R ) <-> ( K S L /\ F R G ) )