Metamath Proof Explorer

Theorem elimdelov

Description: Eliminate a hypothesis which is a predicate expressing membership in the result of an operator (deduction version). (Contributed by Paul Chapman, 25-Mar-2008)

Ref Expression
Hypotheses elimdelov.1 ⊢ φ → C ∈ A F B
elimdelov.2 ⊢ Z ∈ X F Y
Assertion elimdelov ⊢ if φ C Z ∈ if φ A X F if φ B Y

Proof

Step Hyp Ref Expression
1 elimdelov.1 ⊢ φ → C ∈ A F B
2 elimdelov.2 ⊢ Z ∈ X F Y
3 iftrue ⊢ φ → if φ C Z = C
4 iftrue ⊢ φ → if φ A X = A
5 iftrue ⊢ φ → if φ B Y = B
6 4 5 oveq12d ⊢ φ → if φ A X F if φ B Y = A F B
7 1 3 6 3eltr4d ⊢ φ → if φ C Z ∈ if φ A X F if φ B Y
8 iffalse ⊢ ¬ φ → if φ C Z = Z
9 8 2 eqeltrdi ⊢ ¬ φ → if φ C Z ∈ X F Y
10 iffalse ⊢ ¬ φ → if φ A X = X
11 iffalse ⊢ ¬ φ → if φ B Y = Y
12 10 11 oveq12d ⊢ ¬ φ → if φ A X F if φ B Y = X F Y
13 9 12 eleqtrrd ⊢ ¬ φ → if φ C Z ∈ if φ A X F if φ B Y
14 7 13 pm2.61i ⊢ if φ C Z ∈ if φ A X F if φ B Y