Theorem ifexd

Description: Existence of the conditional operator (deduction form). (Contributed by SN, 26-Jul-2024)

	Ref	Expression
Hypotheses	ifexd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ifexd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	ifexd	⊢ ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		ifexd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ifexd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3	1	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
4	2	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
5	3 4	ifcld	⊢ ( 𝜑 → if ( 𝜓 , 𝐴 , 𝐵 ) ∈ V )