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 ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) }

Proof

Step	Hyp	Ref	Expression
1		bj-df-ifc	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) }
2		df-ifp	⊢ ( if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) )
3	2	abbii	⊢ { 𝑥 ∣ if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) } = { 𝑥 ∣ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) }
4	1 3	eqtri	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) }