This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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