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 eqtrid 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