# Metamath Proof Explorer

## Theorem aov0nbovbi

Description: The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion aov0nbovbi ${⊢}\varnothing \notin {C}\to \left((({A}{F}{B}))\in {C}↔{A}{F}{B}\in {C}\right)$

### Proof

Step Hyp Ref Expression
1 afv0nbfvbi ${⊢}\varnothing \notin {C}\to \left(\left({F}\mathrm{\text{'}\text{'}\text{'}}⟨{A},{B}⟩\right)\in {C}↔{F}\left(⟨{A},{B}⟩\right)\in {C}\right)$
2 df-aov ${⊢}(({A}{F}{B}))=\left({F}\mathrm{\text{'}\text{'}\text{'}}⟨{A},{B}⟩\right)$
3 2 eleq1i ${⊢}(({A}{F}{B}))\in {C}↔\left({F}\mathrm{\text{'}\text{'}\text{'}}⟨{A},{B}⟩\right)\in {C}$
4 df-ov ${⊢}{A}{F}{B}={F}\left(⟨{A},{B}⟩\right)$
5 4 eleq1i ${⊢}{A}{F}{B}\in {C}↔{F}\left(⟨{A},{B}⟩\right)\in {C}$
6 1 3 5 3bitr4g ${⊢}\varnothing \notin {C}\to \left((({A}{F}{B}))\in {C}↔{A}{F}{B}\in {C}\right)$