Theorem bj-dfif

Description: Alternate definition of the conditional operator for classes, which used to be the main definition. (Contributed by BJ, 26-Dec-2023) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-dfif	|- if ( ph , A , B ) = { x | ( ( ph /\ x e. A ) \/ ( -. ph /\ x e. B ) ) }

Proof

Step	Hyp	Ref	Expression
1		bj-df-ifc	|- if ( ph , A , B ) = { x | if- ( ph , x e. A , x e. B ) }
2		df-ifp	|- ( if- ( ph , x e. A , x e. B ) <-> ( ( ph /\ x e. A ) \/ ( -. ph /\ x e. B ) ) )
3	2	abbii	|- { x | if- ( ph , x e. A , x e. B ) } = { x | ( ( ph /\ x e. A ) \/ ( -. ph /\ x e. B ) ) }
4	1 3	eqtri	|- if ( ph , A , B ) = { x | ( ( ph /\ x e. A ) \/ ( -. ph /\ x e. B ) ) }