falseral0

Description: A false statement can only be true for elements of an empty set. (Contributed by AV, 30-Oct-2020) (Proof shortened by TM, 16-Feb-2026)

		Ref	Expression
	Assertion	falseral0	⊢ ( ( ∀ 𝑥 ¬ 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		alral	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 )
2		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → ⊥ ) )
3	2	ral2imi	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 ⊥ ) )
4	3	imp	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ⊥ )
5	1 4	sylan	⊢ ( ( ∀ 𝑥 ¬ 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ⊥ )
6		fal	⊢ ¬ ⊥
7	6	ralf0	⊢ ( ∀ 𝑥 ∈ 𝐴 ⊥ ↔ 𝐴 = ∅ )
8	5 7	sylib	⊢ ( ( ∀ 𝑥 ¬ 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → 𝐴 = ∅ )

Metamath Proof Explorer

Theorem falseral0

Proof