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

Metamath Proof Explorer

Theorem ifeq1

Description: Equality theorem for conditional operator. (Contributed by NM, 1-Sep-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion ifeq1 ⊢ A = B → if φ A C = if φ B C

Proof

Step Hyp Ref Expression
1 rabeq ⊢ A = B → x ∈ A | φ = x ∈ B | φ
2 1 uneq1d ⊢ A = B → x ∈ A | φ ∪ x ∈ C | ¬ φ = x ∈ B | φ ∪ x ∈ C | ¬ φ
3 dfif6 ⊢ if φ A C = x ∈ A | φ ∪ x ∈ C | ¬ φ
4 dfif6 ⊢ if φ B C = x ∈ B | φ ∪ x ∈ C | ¬ φ
5 2 3 4 3eqtr4g ⊢ A = B → if φ A C = if φ B C