Theorem ifexg 4472

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  Vcvv 3441  ifcif 4425

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-if 4426

This theorem is referenced by:  fsuppmptif  8847  cantnfp1lem1  9125  cantnfp1lem3  9127  symgextfv  18538  pmtrfv  18572  evlslem3  20752  marrepeval  21168  gsummatr01lem3  21262  stdbdmetval  23121  stdbdxmet  23122  ellimc2  24480  psgnfzto1stlem  30792  cdleme31fv  37686  sge0val  43005  hsphoival  43218  hspmbllem2  43266