Theorem ifex

Description: Existence of the conditional operator (inference form). (Contributed by NM, 2-Sep-2004)

	Ref	Expression
Hypotheses	ifex.1	⊢ 𝐴 ∈ V
	ifex.2	⊢ 𝐵 ∈ V
Assertion	ifex	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		ifex.1	⊢ 𝐴 ∈ V
2		ifex.2	⊢ 𝐵 ∈ V
3	1 2	ifcli	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) ∈ V