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

Proof

Step	Hyp	Ref	Expression
1		df-if	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) }
2		ancom	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
3		ancom	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ↔ ( ¬ 𝜑 ∧ 𝑥 ∈ 𝐵 ) )
4	2 3	orbi12i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) )
5		df-ifp	⊢ ( if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑥 ∈ 𝐵 ) ) )
6	4 5	bitr4i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) ↔ if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) )
7	6	abbii	⊢ { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝜑 ) ) } = { 𝑥 ∣ if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) }
8	1 7	eqtri	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) }