Theorem elcnvlem

Description: Two ways to say a set is a member of the converse of a class. (Contributed by RP, 19-Aug-2020)

	Ref	Expression
Hypothesis	elcnvlem.f	$$⊢F=\left(x\in \left(\mathrm{V}\times \mathrm{V}\right)⟼⟨2^{nd}\left(x\right),1^{st}\left(x\right)⟩\right)$$
Assertion	elcnvlem	$$⊢A\in B^{-1}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge F\left(A\right)\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elcnvlem.f	$$⊢F=\left(x\in \left(\mathrm{V}\times \mathrm{V}\right)⟼⟨2^{nd}\left(x\right),1^{st}\left(x\right)⟩\right)$$
2		elcnv2	$$⊢A\in B^{-1}\leftrightarrow \exists u\exists v\left(A=⟨u,v⟩\wedge ⟨v,u⟩\in B\right)$$
3		fveq2	$$⊢A=⟨u,v⟩\to F\left(A\right)=F\left(⟨u,v⟩\right)$$
4		vex	$$⊢u\in \mathrm{V}$$
5		vex	$$⊢v\in \mathrm{V}$$
6	4 5	opelvv	$$⊢⟨u,v⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
7	4 5	op2ndd	$$⊢x=⟨u,v⟩\to 2^{nd}\left(x\right)=v$$
8	4 5	op1std	$$⊢x=⟨u,v⟩\to 1^{st}\left(x\right)=u$$
9	7 8	opeq12d	$$⊢x=⟨u,v⟩\to ⟨2^{nd}\left(x\right),1^{st}\left(x\right)⟩=⟨v,u⟩$$
10		opex	$$⊢⟨v,u⟩\in \mathrm{V}$$
11	9 1 10	fvmpt	$$⊢⟨u,v⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\to F\left(⟨u,v⟩\right)=⟨v,u⟩$$
12	6 11	ax-mp	$$⊢F\left(⟨u,v⟩\right)=⟨v,u⟩$$
13	3 12	eqtrdi	$$⊢A=⟨u,v⟩\to F\left(A\right)=⟨v,u⟩$$
14	13	eleq1d	$$⊢A=⟨u,v⟩\to \left(F\left(A\right)\in B\leftrightarrow ⟨v,u⟩\in B\right)$$
15	14	copsex2gb	$$⊢\exists u\exists v\left(A=⟨u,v⟩\wedge ⟨v,u⟩\in B\right)\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge F\left(A\right)\in B\right)$$
16	2 15	bitri	$$⊢A\in B^{-1}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge F\left(A\right)\in B\right)$$