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

Metamath Proof Explorer

Theorem nfof

Description: Hypothesis builder for function operation. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Hypothesis nfof.1 ⊢ Ⅎ _ x R
Assertion nfof ⊢ Ⅎ _ x ∘ f ⁡ R

Proof

Step Hyp Ref Expression
1 nfof.1 ⊢ Ⅎ _ x R
2 df-of ⊢ ∘ f ⁡ R = u ∈ V , v ∈ V ⟼ w ∈ dom ⁡ u ∩ dom ⁡ v ⟼ u ⁡ w R v ⁡ w
3 nfcv ⊢ Ⅎ _ x V
4 nfcv ⊢ Ⅎ _ x dom ⁡ u ∩ dom ⁡ v
5 nfcv ⊢ Ⅎ _ x u ⁡ w
6 nfcv ⊢ Ⅎ _ x v ⁡ w
7 5 1 6 nfov ⊢ Ⅎ _ x u ⁡ w R v ⁡ w
8 4 7 nfmpt ⊢ Ⅎ _ x w ∈ dom ⁡ u ∩ dom ⁡ v ⟼ u ⁡ w R v ⁡ w
9 3 3 8 nfmpo ⊢ Ⅎ _ x u ∈ V , v ∈ V ⟼ w ∈ dom ⁡ u ∩ dom ⁡ v ⟼ u ⁡ w R v ⁡ w
10 2 9 nfcxfr ⊢ Ⅎ _ x ∘ f ⁡ R