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 ⊢ A ∈ C ∧ B ∈ D → if φ A B ∈ A B

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ C → A ∈ V
2 elex ⊢ B ∈ D → B ∈ V
3 ifcl ⊢ A ∈ V ∧ B ∈ V → if φ A B ∈ V
4 ifeqor ⊢ if φ A B = A ∨ if φ A B = B
5 elprg ⊢ if φ A B ∈ V → if φ A B ∈ A B ↔ if φ A B = A ∨ if φ A B = B
6 4 5 mpbiri ⊢ if φ A B ∈ V → if φ A B ∈ A B
7 3 6 syl ⊢ A ∈ V ∧ B ∈ V → if φ A B ∈ A B
8 1 2 7 syl2an ⊢ A ∈ C ∧ B ∈ D → if φ A B ∈ A B