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

Metamath Proof Explorer

Theorem offveqb

Description: Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Hypotheses offveq.1 ⊢ φ → A ∈ V
offveq.2 ⊢ φ → F Fn A
offveq.3 ⊢ φ → G Fn A
offveq.4 ⊢ φ → H Fn A
offveq.5 ⊢ φ ∧ x ∈ A → F ⁡ x = B
offveq.6 ⊢ φ ∧ x ∈ A → G ⁡ x = C
Assertion offveqb ⊢ φ → H = F R f G ↔ ∀ x ∈ A H ⁡ x = B R C

Proof

Step Hyp Ref Expression
1 offveq.1 ⊢ φ → A ∈ V
2 offveq.2 ⊢ φ → F Fn A
3 offveq.3 ⊢ φ → G Fn A
4 offveq.4 ⊢ φ → H Fn A
5 offveq.5 ⊢ φ ∧ x ∈ A → F ⁡ x = B
6 offveq.6 ⊢ φ ∧ x ∈ A → G ⁡ x = C
7 dffn5 ⊢ H Fn A ↔ H = x ∈ A ⟼ H ⁡ x
8 4 7 sylib ⊢ φ → H = x ∈ A ⟼ H ⁡ x
9 inidm ⊢ A ∩ A = A
10 2 3 1 1 9 5 6 offval ⊢ φ → F R f G = x ∈ A ⟼ B R C
11 8 10 eqeq12d ⊢ φ → H = F R f G ↔ x ∈ A ⟼ H ⁡ x = x ∈ A ⟼ B R C
12 fvexd ⊢ φ → H ⁡ x ∈ V
13 12 ralrimivw ⊢ φ → ∀ x ∈ A H ⁡ x ∈ V
14 mpteqb ⊢ ∀ x ∈ A H ⁡ x ∈ V → x ∈ A ⟼ H ⁡ x = x ∈ A ⟼ B R C ↔ ∀ x ∈ A H ⁡ x = B R C
15 13 14 syl ⊢ φ → x ∈ A ⟼ H ⁡ x = x ∈ A ⟼ B R C ↔ ∀ x ∈ A H ⁡ x = B R C
16 11 15 bitrd ⊢ φ → H = F R f G ↔ ∀ x ∈ A H ⁡ x = B R C