Theorem aov0nbovbi 42096

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.)

Assertion

Ref	Expression
aov0nbovbi	⊢ (∅ ∉ 𝐶 → ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶))

Proof of Theorem aov0nbovbi

Step	Hyp	Ref	Expression
1		afv0nbfvbi 42052	. 2 ⊢ (∅ ∉ 𝐶 → ((𝐹'''⟨𝐴, 𝐵⟩) ∈ 𝐶 ↔ (𝐹‘⟨𝐴, 𝐵⟩) ∈ 𝐶))
2		df-aov 42022	. . 3 ⊢ ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
3	2	eleq1i 2896	. 2 ⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐹'''⟨𝐴, 𝐵⟩) ∈ 𝐶)
4		df-ov 6907	. . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
5	4	eleq1i 2896	. 2 ⊢ ((𝐴𝐹𝐵) ∈ 𝐶 ↔ (𝐹‘⟨𝐴, 𝐵⟩) ∈ 𝐶)
6	1, 3, 5	3bitr4g 306	1 ⊢ (∅ ∉ 𝐶 → ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶))

Syntax hints:   → wi 4   ↔ wb 198   ∈ wcel 2166   ∉ wnel 3101  ∅c0 4143  ⟨cop 4402  ‘cfv 6122  (class class class)co 6904  '''cafv 42018   ((caov 42019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-fal 1672  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-uni 4658  df-int 4697  df-br 4873  df-opab 4935  df-id 5249  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-res 5353  df-iota 6085  df-fun 6124  df-fv 6130  df-ov 6907  df-aiota 41981  df-dfat 42020  df-afv 42021  df-aov 42022

This theorem is referenced by: (None)