Theorem falseral0

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

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

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
2		19.26	⊢ ( ∀ 𝑥 ( ¬ 𝜑 ∧ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ↔ ( ∀ 𝑥 ¬ 𝜑 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) )
3		con3	⊢ ( ( 𝑥 ∈ 𝐴 → 𝜑 ) → ( ¬ 𝜑 → ¬ 𝑥 ∈ 𝐴 ) )
4	3	impcom	⊢ ( ( ¬ 𝜑 ∧ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ¬ 𝑥 ∈ 𝐴 )
5	4	alimi	⊢ ( ∀ 𝑥 ( ¬ 𝜑 ∧ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 )
6		alnex	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ 𝐴 ↔ ¬ ∃ 𝑥 𝑥 ∈ 𝐴 )
7	5 6	sylib	⊢ ( ∀ 𝑥 ( ¬ 𝜑 ∧ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → ¬ ∃ 𝑥 𝑥 ∈ 𝐴 )
8		notnotb	⊢ ( 𝐴 = ∅ ↔ ¬ ¬ 𝐴 = ∅ )
9		neq0	⊢ ( ¬ 𝐴 = ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
10	8 9	xchbinx	⊢ ( 𝐴 = ∅ ↔ ¬ ∃ 𝑥 𝑥 ∈ 𝐴 )
11	7 10	sylibr	⊢ ( ∀ 𝑥 ( ¬ 𝜑 ∧ ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → 𝐴 = ∅ )
12	2 11	sylbir	⊢ ( ( ∀ 𝑥 ¬ 𝜑 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) → 𝐴 = ∅ )
13	1 12	sylan2b	⊢ ( ( ∀ 𝑥 ¬ 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) → 𝐴 = ∅ )