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	|- ( X e. if ( ph , A , B ) <-> if- ( ph , X e. A , X e. B ) )

Proof

Step	Hyp	Ref	Expression
1		bj-df-ifc	|- if ( ph , A , B ) = { x | if- ( ph , x e. A , x e. B ) }
2	1	eleq2i	|- ( X e. if ( ph , A , B ) <-> X e. { x | if- ( ph , x e. A , x e. B ) } )
3		df-ifp	|- ( if- ( ph , X e. A , X e. B ) <-> ( ( ph /\ X e. A ) \/ ( -. ph /\ X e. B ) ) )
4		elex	|- ( X e. A -> X e. _V )
5	4	adantl	|- ( ( ph /\ X e. A ) -> X e. _V )
6		elex	|- ( X e. B -> X e. _V )
7	6	adantl	|- ( ( -. ph /\ X e. B ) -> X e. _V )
8	5 7	jaoi	|- ( ( ( ph /\ X e. A ) \/ ( -. ph /\ X e. B ) ) -> X e. _V )
9	3 8	sylbi	|- ( if- ( ph , X e. A , X e. B ) -> X e. _V )
10		eleq1	|- ( x = X -> ( x e. A <-> X e. A ) )
11		eleq1	|- ( x = X -> ( x e. B <-> X e. B ) )
12	10 11	ifpbi23d	|- ( x = X -> ( if- ( ph , x e. A , x e. B ) <-> if- ( ph , X e. A , X e. B ) ) )
13	9 12	elab3	|- ( X e. { x | if- ( ph , x e. A , x e. B ) } <-> if- ( ph , X e. A , X e. B ) )
14	2 13	bitri	|- ( X e. if ( ph , A , B ) <-> if- ( ph , X e. A , X e. B ) )