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

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)

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