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

Theorem ifexg 4497
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 3498 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 3498 . 2 (𝐵𝑊𝐵 ∈ V)
3 ifcl 4494 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → if(𝜑, 𝐴, 𝐵) ∈ V)
41, 2, 3syl2an 598 1 ((𝐴𝑉𝐵𝑊) → if(𝜑, 𝐴, 𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2115  Vcvv 3480  ifcif 4450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-if 4451
This theorem is referenced by:  fsuppmptif  8860  cantnfp1lem1  9138  cantnfp1lem3  9140  symgextfv  18546  pmtrfv  18580  evlslem3  20759  marrepeval  21175  gsummatr01lem3  21269  stdbdmetval  23128  stdbdxmet  23129  ellimc2  24487  psgnfzto1stlem  30778  cdleme31fv  37635  sge0val  42936  hsphoival  43149  hspmbllem2  43197
  Copyright terms: Public domain W3C validator