Metamath Proof Explorer

Theorem unxpdomlem1

Description: Lemma for unxpdom . (Trivial substitution proof.) (Contributed by Mario Carneiro, 13-Jan-2013)

Ref Expression
Hypotheses unxpdomlem1.1 ⊢ F = x ∈ a ∪ b ⟼ G
unxpdomlem1.2 ⊢ G = if x ∈ a x if x = m t s if x = t n m x
Assertion unxpdomlem1 ⊢ z ∈ a ∪ b → F ⁡ z = if z ∈ a z if z = m t s if z = t n m z

Proof

Step Hyp Ref Expression
1 unxpdomlem1.1 ⊢ F = x ∈ a ∪ b ⟼ G
2 unxpdomlem1.2 ⊢ G = if x ∈ a x if x = m t s if x = t n m x
3 elequ1 ⊢ x = z → x ∈ a ↔ z ∈ a
4 opeq1 ⊢ x = z → x if x = m t s = z if x = m t s
5 equequ1 ⊢ x = z → x = m ↔ z = m
6 5 ifbid ⊢ x = z → if x = m t s = if z = m t s
7 6 opeq2d ⊢ x = z → z if x = m t s = z if z = m t s
8 4 7 eqtrd ⊢ x = z → x if x = m t s = z if z = m t s
9 equequ1 ⊢ x = z → x = t ↔ z = t
10 9 ifbid ⊢ x = z → if x = t n m = if z = t n m
11 10 opeq1d ⊢ x = z → if x = t n m x = if z = t n m x
12 opeq2 ⊢ x = z → if z = t n m x = if z = t n m z
13 11 12 eqtrd ⊢ x = z → if x = t n m x = if z = t n m z
14 3 8 13 ifbieq12d ⊢ x = z → if x ∈ a x if x = m t s if x = t n m x = if z ∈ a z if z = m t s if z = t n m z
15 2 14 syl5eq ⊢ x = z → G = if z ∈ a z if z = m t s if z = t n m z
16 opex ⊢ z if z = m t s ∈ V
17 opex ⊢ if z = t n m z ∈ V
18 16 17 ifex ⊢ if z ∈ a z if z = m t s if z = t n m z ∈ V
19 15 1 18 fvmpt ⊢ z ∈ a ∪ b → F ⁡ z = if z ∈ a z if z = m t s if z = t n m z