Theorem cnvexg

Description: The converse of a set is a set. Corollary 6.8(1) of TakeutiZaring p. 26. (Contributed by NM, 17-Mar-1998)

	Ref	Expression
Assertion	cnvexg	⊢ ( 𝐴 ∈ 𝑉 → ◡ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ 𝐴
2		relssdmrn	⊢ ( Rel ◡ 𝐴 → ◡ 𝐴 ⊆ ( dom ◡ 𝐴 × ran ◡ 𝐴 ) )
3	1 2	ax-mp	⊢ ◡ 𝐴 ⊆ ( dom ◡ 𝐴 × ran ◡ 𝐴 )
4		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
5		rnexg	⊢ ( 𝐴 ∈ 𝑉 → ran 𝐴 ∈ V )
6	4 5	eqeltrrid	⊢ ( 𝐴 ∈ 𝑉 → dom ◡ 𝐴 ∈ V )
7		dfdm4	⊢ dom 𝐴 = ran ◡ 𝐴
8		dmexg	⊢ ( 𝐴 ∈ 𝑉 → dom 𝐴 ∈ V )
9	7 8	eqeltrrid	⊢ ( 𝐴 ∈ 𝑉 → ran ◡ 𝐴 ∈ V )
10	6 9	xpexd	⊢ ( 𝐴 ∈ 𝑉 → ( dom ◡ 𝐴 × ran ◡ 𝐴 ) ∈ V )
11		ssexg	⊢ ( ( ◡ 𝐴 ⊆ ( dom ◡ 𝐴 × ran ◡ 𝐴 ) ∧ ( dom ◡ 𝐴 × ran ◡ 𝐴 ) ∈ V ) → ◡ 𝐴 ∈ V )
12	3 10 11	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ◡ 𝐴 ∈ V )