Theorem bj-df-ifc

Description: Candidate definition for the conditional operator for classes. This is in line with the definition of a class as the extension of a predicate in df-clab . We reprove the current df-if from it in bj-dfif . (Contributed by BJ, 20-Sep-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-df-ifc	|- if ( ph , A , B ) = { x | if- ( ph , x e. A , x e. B ) }

Proof

Step	Hyp	Ref	Expression
1		df-if	|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) }
2		ancom	|- ( ( x e. A /\ ph ) <-> ( ph /\ x e. A ) )
3		ancom	|- ( ( x e. B /\ -. ph ) <-> ( -. ph /\ x e. B ) )
4	2 3	orbi12i	|- ( ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) <-> ( ( ph /\ x e. A ) \/ ( -. ph /\ x e. B ) ) )
5		df-ifp	|- ( if- ( ph , x e. A , x e. B ) <-> ( ( ph /\ x e. A ) \/ ( -. ph /\ x e. B ) ) )
6	4 5	bitr4i	|- ( ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) <-> if- ( ph , x e. A , x e. B ) )
7	6	abbii	|- { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } = { x | if- ( ph , x e. A , x e. B ) }
8	1 7	eqtri	|- if ( ph , A , B ) = { x | if- ( ph , x e. A , x e. B ) }