Theorem ifpr

Description: Membership of a conditional operator in an unordered pair. (Contributed by NM, 17-Jun-2007)

	Ref	Expression
Assertion	ifpr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → if ( 𝜑 , 𝐴 , 𝐵 ) ∈ { 𝐴 , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V )
2		elex	⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V )
3		ifcl	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → if ( 𝜑 , 𝐴 , 𝐵 ) ∈ V )
4		ifeqor	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ∨ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
5		elprg	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) ∈ V → ( if ( 𝜑 , 𝐴 , 𝐵 ) ∈ { 𝐴 , 𝐵 } ↔ ( if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 ∨ if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 ) ) )
6	4 5	mpbiri	⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) ∈ V → if ( 𝜑 , 𝐴 , 𝐵 ) ∈ { 𝐴 , 𝐵 } )
7	3 6	syl	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → if ( 𝜑 , 𝐴 , 𝐵 ) ∈ { 𝐴 , 𝐵 } )
8	1 2 7	syl2an	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → if ( 𝜑 , 𝐴 , 𝐵 ) ∈ { 𝐴 , 𝐵 } )