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

Metamath Proof Explorer

Theorem nfco

Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999)

Ref Expression
Hypotheses nfco.1 ⊢ Ⅎ _ x A
nfco.2 ⊢ Ⅎ _ x B
Assertion nfco ⊢ Ⅎ _ x A ∘ B

Proof

Step Hyp Ref Expression
1 nfco.1 ⊢ Ⅎ _ x A
2 nfco.2 ⊢ Ⅎ _ x B
3 df-co ⊢ A ∘ B = y z | ∃ w y B w ∧ w A z
4 nfcv ⊢ Ⅎ _ x y
5 nfcv ⊢ Ⅎ _ x w
6 4 2 5 nfbr ⊢ Ⅎ x y B w
7 nfcv ⊢ Ⅎ _ x z
8 5 1 7 nfbr ⊢ Ⅎ x w A z
9 6 8 nfan ⊢ Ⅎ x y B w ∧ w A z
10 9 nfex ⊢ Ⅎ x ∃ w y B w ∧ w A z
11 10 nfopab ⊢ Ⅎ _ x y z | ∃ w y B w ∧ w A z
12 3 11 nfcxfr ⊢ Ⅎ _ x A ∘ B