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

Metamath Proof Explorer

Theorem nfofr

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

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

Proof

Step Hyp Ref Expression
1 nfof.1 ⊢ Ⅎ _ x R
2 df-ofr ⊢ ∘ r ⁡ R = u v | ∀ w ∈ dom ⁡ u ∩ dom ⁡ v u ⁡ w R v ⁡ w
3 nfcv ⊢ Ⅎ _ x dom ⁡ u ∩ dom ⁡ v
4 nfcv ⊢ Ⅎ _ x u ⁡ w
5 nfcv ⊢ Ⅎ _ x v ⁡ w
6 4 1 5 nfbr ⊢ Ⅎ x u ⁡ w R v ⁡ w
7 3 6 nfralw ⊢ Ⅎ x ∀ w ∈ dom ⁡ u ∩ dom ⁡ v u ⁡ w R v ⁡ w
8 7 nfopab ⊢ Ⅎ _ x u v | ∀ w ∈ dom ⁡ u ∩ dom ⁡ v u ⁡ w R v ⁡ w
9 2 8 nfcxfr ⊢ Ⅎ _ x ∘ r ⁡ R