This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prtlem100

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

Ref Expression
Assertion prtlem100 ( ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ≠ ∅ ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) ) )
2 eldifsn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∅ ) )
3 2 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) )
4 ne0i ⊢ ( 𝐵 ∈ 𝑥 → 𝑥 ≠ ∅ )
5 4 pm4.71ri ⊢ ( 𝐵 ∈ 𝑥 ↔ ( 𝑥 ≠ ∅ ∧ 𝐵 ∈ 𝑥 ) )
6 5 anbi1i ⊢ ( ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝐵 ∈ 𝑥 ) ∧ 𝜑 ) )
7 anass ⊢ ( ( ( 𝑥 ≠ ∅ ∧ 𝐵 ∈ 𝑥 ) ∧ 𝜑 ) ↔ ( 𝑥 ≠ ∅ ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) )
8 6 7 bitri ⊢ ( ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ↔ ( 𝑥 ≠ ∅ ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) )
9 8 anbi2i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ≠ ∅ ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) ) )
10 1 3 9 3bitr4ri ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ∧ ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ) )
11 10 rexbii2 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) )