Theorem bj-ififc

Description: A biconditional connecting the conditional operator for propositions and the conditional operator for classes. Note that there is no sethood hypothesis on X : it is implied by either side. (Contributed by BJ, 24-Sep-2019) Generalize statement from setvar x to class X . (Revised by BJ, 26-Dec-2023)

	Ref	Expression
Assertion	bj-ififc	⊢ ( 𝑋 ∈ if ( 𝜑 , 𝐴 , 𝐵 ) ↔ if- ( 𝜑 , 𝑋 ∈ 𝐴 , 𝑋 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-df-ifc	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = { 𝑥 ∣ if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) }
2	1	eleq2i	⊢ ( 𝑋 ∈ if ( 𝜑 , 𝐴 , 𝐵 ) ↔ 𝑋 ∈ { 𝑥 ∣ if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) } )
3		df-ifp	⊢ ( if- ( 𝜑 , 𝑋 ∈ 𝐴 , 𝑋 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑋 ∈ 𝐵 ) ) )
4		elex	⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ V )
5	4	adantl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ V )
6		elex	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ V )
7	6	adantl	⊢ ( ( ¬ 𝜑 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ V )
8	5 7	jaoi	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) ∨ ( ¬ 𝜑 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ V )
9	3 8	sylbi	⊢ ( if- ( 𝜑 , 𝑋 ∈ 𝐴 , 𝑋 ∈ 𝐵 ) → 𝑋 ∈ V )
10		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
11		eleq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵 ) )
12	10 11	ifpbi23d	⊢ ( 𝑥 = 𝑋 → ( if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) ↔ if- ( 𝜑 , 𝑋 ∈ 𝐴 , 𝑋 ∈ 𝐵 ) ) )
13	9 12	elab3	⊢ ( 𝑋 ∈ { 𝑥 ∣ if- ( 𝜑 , 𝑥 ∈ 𝐴 , 𝑥 ∈ 𝐵 ) } ↔ if- ( 𝜑 , 𝑋 ∈ 𝐴 , 𝑋 ∈ 𝐵 ) )
14	2 13	bitri	⊢ ( 𝑋 ∈ if ( 𝜑 , 𝐴 , 𝐵 ) ↔ if- ( 𝜑 , 𝑋 ∈ 𝐴 , 𝑋 ∈ 𝐵 ) )