Description: Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfof.1 | ⊢ Ⅎ 𝑥 𝑅 | |
Assertion | nfofr | ⊢ Ⅎ 𝑥 ∘r 𝑅 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfof.1 | ⊢ Ⅎ 𝑥 𝑅 | |
2 | df-ofr | ⊢ ∘r 𝑅 = { 〈 𝑢 , 𝑣 〉 ∣ ∀ 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) } | |
3 | nfcv | ⊢ Ⅎ 𝑥 ( dom 𝑢 ∩ dom 𝑣 ) | |
4 | nfcv | ⊢ Ⅎ 𝑥 ( 𝑢 ‘ 𝑤 ) | |
5 | nfcv | ⊢ Ⅎ 𝑥 ( 𝑣 ‘ 𝑤 ) | |
6 | 4 1 5 | nfbr | ⊢ Ⅎ 𝑥 ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) |
7 | 3 6 | nfralw | ⊢ Ⅎ 𝑥 ∀ 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) |
8 | 7 | nfopab | ⊢ Ⅎ 𝑥 { 〈 𝑢 , 𝑣 〉 ∣ ∀ 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) } |
9 | 2 8 | nfcxfr | ⊢ Ⅎ 𝑥 ∘r 𝑅 |