Metamath Proof Explorer


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 if φ A B if- φ X A X B

Proof

Step Hyp Ref Expression
1 bj-df-ifc if φ A B = x | if- φ x A x B
2 1 eleq2i X if φ A B X x | if- φ x A x B
3 df-ifp if- φ X A X B φ X A ¬ φ X B
4 elex X A X V
5 4 adantl φ X A X V
6 elex X B X V
7 6 adantl ¬ φ X B X V
8 5 7 jaoi φ X A ¬ φ X B X V
9 3 8 sylbi if- φ X A X B X V
10 eleq1 x = X x A X A
11 eleq1 x = X x B X B
12 10 11 ifpbi23d x = X if- φ x A x B if- φ X A X B
13 9 12 elab3 X x | if- φ x A x B if- φ X A X B
14 2 13 bitri X if φ A B if- φ X A X B