oe0lem

Description: A helper lemma for oe0 and others. (Contributed by NM, 6-Jan-2005)

	Ref	Expression
Hypotheses	oe0lem.1	$⊢ (φ \land A = \emptyset) \to ψ$
	oe0lem.2	$⊢ ((A \in On \land φ) \land \emptyset \in A) \to ψ$
Assertion	oe0lem	$⊢ (A \in On \land φ) \to ψ$

Step	Hyp	Ref	Expression
1		oe0lem.1	$⊢ (φ \land A = \emptyset) \to ψ$
2		oe0lem.2	$⊢ ((A \in On \land φ) \land \emptyset \in A) \to ψ$
3	1	ex	$⊢ φ \to (A = \emptyset \to ψ)$
4	3	adantl	$⊢ (A \in On \land φ) \to (A = \emptyset \to ψ)$
5		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
6	5	adantr	$⊢ (A \in On \land φ) \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
7	2	ex	$⊢ (A \in On \land φ) \to (\emptyset \in A \to ψ)$
8	6 7	sylbird	$⊢ (A \in On \land φ) \to (A \neq \emptyset \to ψ)$
9	4 8	pm2.61dne	$⊢ (A \in On \land φ) \to ψ$

Metamath Proof Explorer