![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifexg | Structured version Visualization version GIF version |
Description: Conditional operator existence. (Contributed by NM, 21-Mar-2011.) (Proof shortened by BJ, 1-Sep-2022.) |
Ref | Expression |
---|---|
ifexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3413 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | elex 3413 | . 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) | |
3 | ifcl 4350 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → if(𝜑, 𝐴, 𝐵) ∈ V) | |
4 | 1, 2, 3 | syl2an 589 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2106 Vcvv 3397 ifcif 4306 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-12 2162 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-v 3399 df-if 4307 |
This theorem is referenced by: fsuppmptif 8593 cantnfp1lem1 8872 cantnfp1lem3 8874 symgextfv 18221 pmtrfv 18255 evlslem3 19910 marrepeval 20774 gsummatr01lem3 20869 stdbdmetval 22727 stdbdxmet 22728 ellimc2 24078 psgnfzto1stlem 30448 cdleme31fv 36528 sge0val 41489 hsphoival 41702 hspmbllem2 41750 |
Copyright terms: Public domain | W3C validator |