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	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ( 𝐵 ∈ 𝑥 ∧ 𝜑 ) )