Theorem 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)

	Ref	Expression
Assertion	cnv0	⊢ ◡ ∅ = ∅

Proof

Step	Hyp	Ref	Expression
1		br0	⊢ ¬ 𝑦 ∅ 𝑧
2	1	intnan	⊢ ¬ ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 )
3	2	nex	⊢ ¬ ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 )
4	3	nex	⊢ ¬ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 )
5		df-cnv	⊢ ◡ ∅ = { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝑦 ∅ 𝑧 }
6		df-opab	⊢ { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝑦 ∅ 𝑧 } = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) }
7	5 6	eqtri	⊢ ◡ ∅ = { 𝑥 ∣ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) }
8	7	abeq2i	⊢ ( 𝑥 ∈ ◡ ∅ ↔ ∃ 𝑧 ∃ 𝑦 ( 𝑥 = ⟨ 𝑧 , 𝑦 ⟩ ∧ 𝑦 ∅ 𝑧 ) )
9	4 8	mtbir	⊢ ¬ 𝑥 ∈ ◡ ∅
10	9	nel0	⊢ ◡ ∅ = ∅