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

Metamath Proof Explorer

Theorem prnzg

Description: A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011) (Proof shortened by JJ, 23-Jul-2021)

Ref Expression
Assertion prnzg ⊢ A ∈ V → A B ≠ ∅

Proof

Step Hyp Ref Expression
1 prid1g ⊢ A ∈ V → A ∈ A B
2 1 ne0d ⊢ A ∈ V → A B ≠ ∅