Description: The value of an operation when the one of the arguments is a proper class, analogous to ovprc . (Contributed by Alexander van der Vekens, 26-May-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | aovprc.1 | ⊢ Rel dom 𝐹 | |
| Assertion | aovprc | ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → (( 𝐴 𝐹 𝐵 )) = V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aovprc.1 | ⊢ Rel dom 𝐹 | |
| 2 | df-aov | ⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) | |
| 3 | df-br | ⊢ ( 𝐴 dom 𝐹 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) | |
| 4 | 1 | brrelex12i | ⊢ ( 𝐴 dom 𝐹 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 5 | 3 4 | sylbir | ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
| 6 | ndmafv | ⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V ) | |
| 7 | 5 6 | nsyl5 | ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V ) |
| 8 | 2 7 | syl5eq | ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → (( 𝐴 𝐹 𝐵 )) = V ) |