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	⊢ 𝐹 = ( 𝑥 ∈ ( V × V ) ↦ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ )
Assertion	elcnvlem	⊢ ( 𝐴 ∈ ◡ 𝐵 ↔ ( 𝐴 ∈ ( V × V ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elcnvlem.f	⊢ 𝐹 = ( 𝑥 ∈ ( V × V ) ↦ ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ )
2		elcnv2	⊢ ( 𝐴 ∈ ◡ 𝐵 ↔ ∃ 𝑢 ∃ 𝑣 ( 𝐴 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝐵 ) )
3		fveq2	⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
4		vex	⊢ 𝑢 ∈ V
5		vex	⊢ 𝑣 ∈ V
6	4 5	opelvv	⊢ ⟨ 𝑢 , 𝑣 ⟩ ∈ ( V × V )
7	4 5	op2ndd	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd ‘ 𝑥 ) = 𝑣 )
8	4 5	op1std	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st ‘ 𝑥 ) = 𝑢 )
9	7 8	opeq12d	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ⟨ ( 2nd ‘ 𝑥 ) , ( 1st ‘ 𝑥 ) ⟩ = ⟨ 𝑣 , 𝑢 ⟩ )
10		opex	⊢ ⟨ 𝑣 , 𝑢 ⟩ ∈ V
11	9 1 10	fvmpt	⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ( V × V ) → ( 𝐹 ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ⟨ 𝑣 , 𝑢 ⟩ )
12	6 11	ax-mp	⊢ ( 𝐹 ‘ ⟨ 𝑢 , 𝑣 ⟩ ) = ⟨ 𝑣 , 𝑢 ⟩
13	3 12	eqtrdi	⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐹 ‘ 𝐴 ) = ⟨ 𝑣 , 𝑢 ⟩ )
14	13	eleq1d	⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝐵 ) )
15	14	copsex2gb	⊢ ( ∃ 𝑢 ∃ 𝑣 ( 𝐴 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝐵 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
16	2 15	bitri	⊢ ( 𝐴 ∈ ◡ 𝐵 ↔ ( 𝐴 ∈ ( V × V ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )