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