cnv0

Description: The converse of the empty set. (Contributed by NM, 6-Apr-1998) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) Avoid ax-12 . (Revised by TM, 31-Jan-2026)

		Ref	Expression
	Assertion	cnv0	⊢ ^◡ ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		br0	⊢ ¬ 𝑦 ∅ 𝑧
2	1	intnan	⊢ ¬ ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 )
3	2	nex	⊢ ¬ ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 )
4	3	nex	⊢ ¬ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 )
5		df-cnv	⊢ ^◡ ∅ = { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝑦 ∅ 𝑧 }
6	5	eleq2i	⊢ ( 𝑥 ∈ ^◡ ∅ ↔ 𝑥 ∈ { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝑦 ∅ 𝑧 } )
7		elopabw	⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝑦 ∅ 𝑧 } ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) ) )
8	7	elv	⊢ ( 𝑥 ∈ { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝑦 ∅ 𝑧 } ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) )
9	6 8	bitri	⊢ ( 𝑥 ∈ ^◡ ∅ ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) )
10	4 9	mtbir	⊢ ¬ 𝑥 ∈ ^◡ ∅
11	10	nel0	⊢ ^◡ ∅ = ∅

Metamath Proof Explorer

Theorem cnv0

Proof