Metamath Proof Explorer

Theorem prtlem100

Description: Lemma for prter3 . (Contributed by Rodolfo Medina, 19-Oct-2010)

Ref Expression
Assertion prtlem100 ⊢ ∃ x ∈ A B ∈ x ∧ φ ↔ ∃ x ∈ A ∖ ∅ B ∈ x ∧ φ

Proof

Step Hyp Ref Expression
1 anass ⊢ x ∈ A ∧ x ≠ ∅ ∧ B ∈ x ∧ φ ↔ x ∈ A ∧ x ≠ ∅ ∧ B ∈ x ∧ φ
2 eldifsn ⊢ x ∈ A ∖ ∅ ↔ x ∈ A ∧ x ≠ ∅
3 2 anbi1i ⊢ x ∈ A ∖ ∅ ∧ B ∈ x ∧ φ ↔ x ∈ A ∧ x ≠ ∅ ∧ B ∈ x ∧ φ
4 ne0i ⊢ B ∈ x → x ≠ ∅
5 4 pm4.71ri ⊢ B ∈ x ↔ x ≠ ∅ ∧ B ∈ x
6 5 anbi1i ⊢ B ∈ x ∧ φ ↔ x ≠ ∅ ∧ B ∈ x ∧ φ
7 anass ⊢ x ≠ ∅ ∧ B ∈ x ∧ φ ↔ x ≠ ∅ ∧ B ∈ x ∧ φ
8 6 7 bitri ⊢ B ∈ x ∧ φ ↔ x ≠ ∅ ∧ B ∈ x ∧ φ
9 8 anbi2i ⊢ x ∈ A ∧ B ∈ x ∧ φ ↔ x ∈ A ∧ x ≠ ∅ ∧ B ∈ x ∧ φ
10 1 3 9 3bitr4ri ⊢ x ∈ A ∧ B ∈ x ∧ φ ↔ x ∈ A ∖ ∅ ∧ B ∈ x ∧ φ
11 10 rexbii2 ⊢ ∃ x ∈ A B ∈ x ∧ φ ↔ ∃ x ∈ A ∖ ∅ B ∈ x ∧ φ