Theorem oe0lem

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

	Ref	Expression
Hypotheses	oe0lem.1	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝜓 )
	oe0lem.2	⊢ ( ( ( 𝐴 ∈ On ∧ 𝜑 ) ∧ ∅ ∈ 𝐴 ) → 𝜓 )
Assertion	oe0lem	⊢ ( ( 𝐴 ∈ On ∧ 𝜑 ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		oe0lem.1	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝜓 )
2		oe0lem.2	⊢ ( ( ( 𝐴 ∈ On ∧ 𝜑 ) ∧ ∅ ∈ 𝐴 ) → 𝜓 )
3	1	ex	⊢ ( 𝜑 → ( 𝐴 = ∅ → 𝜓 ) )
4	3	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝜑 ) → ( 𝐴 = ∅ → 𝜓 ) )
5		on0eln0	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
6	5	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝜑 ) → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
7	2	ex	⊢ ( ( 𝐴 ∈ On ∧ 𝜑 ) → ( ∅ ∈ 𝐴 → 𝜓 ) )
8	6 7	sylbird	⊢ ( ( 𝐴 ∈ On ∧ 𝜑 ) → ( 𝐴 ≠ ∅ → 𝜓 ) )
9	4 8	pm2.61dne	⊢ ( ( 𝐴 ∈ On ∧ 𝜑 ) → 𝜓 )