MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifexg Structured version   Visualization version   GIF version

Theorem ifexg 4353
Description: Conditional operator existence. (Contributed by NM, 21-Mar-2011.) (Proof shortened by BJ, 1-Sep-2022.)
Assertion
Ref Expression
ifexg ((𝐴𝑉𝐵𝑊) → if(𝜑, 𝐴, 𝐵) ∈ V)

Proof of Theorem ifexg
StepHypRef Expression
1 elex 3413 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3413 . 2 (𝐵𝑊𝐵 ∈ V)
3 ifcl 4350 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → if(𝜑, 𝐴, 𝐵) ∈ V)
41, 2, 3syl2an 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