Metamath Proof Explorer

Theorem ifexg

Description: Existence of the conditional operator (closed form). (Contributed by NM, 21-Mar-2011) (Proof shortened by BJ, 1-Sep-2022)

Ref Expression
Assertion ifexg ⊢ A ∈ V ∧ B ∈ W → if φ A B ∈ V

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ V ∧ B ∈ W → A ∈ V
2 simpr ⊢ A ∈ V ∧ B ∈ W → B ∈ W
3 1 2 ifexd ⊢ A ∈ V ∧ B ∈ W → if φ A B ∈ V