Theorem ifexg 4516

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 3514	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		elex 3514	. 2 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
3		ifcl 4513	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → if(𝜑, 𝐴, 𝐵) ∈ V)
4	1, 2, 3	syl2an 597	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → if(𝜑, 𝐴, 𝐵) ∈ V)

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  Vcvv 3496  ifcif 4469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498  df-if 4470

This theorem is referenced by:  fsuppmptif  8865  cantnfp1lem1  9143  cantnfp1lem3  9145  symgextfv  18548  pmtrfv  18582  evlslem3  20295  marrepeval  21174  gsummatr01lem3  21268  stdbdmetval  23126  stdbdxmet  23127  ellimc2  24477  psgnfzto1stlem  30744  cdleme31fv  37528  sge0val  42655  hsphoival  42868  hspmbllem2  42916