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	$$⊢\left(A\in V\wedge B\in W\right)\to if\left(\phi ,A,B\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in V\wedge B\in W\right)\to A\in V$$
2		simpr	$$⊢\left(A\in V\wedge B\in W\right)\to B\in W$$
3	1 2	ifexd	$$⊢\left(A\in V\wedge B\in W\right)\to if\left(\phi ,A,B\right)\in \mathrm{V}$$