Theorem elcnvintab

Description: Two ways of saying a set is an element of the converse of the intersection of a class. (Contributed by RP, 19-Aug-2020)

	Ref	Expression
Assertion	elcnvintab	⊢ ( 𝐴 ∈ ◡ ∩ { 𝑥 ∣ 𝜑 } ↔ ( 𝐴 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ ◡ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑦 ∈ ( V × V ) ↦ ⟨ ( 2nd ‘ 𝑦 ) , ( 1st ‘ 𝑦 ) ⟩ ) = ( 𝑦 ∈ ( V × V ) ↦ ⟨ ( 2nd ‘ 𝑦 ) , ( 1st ‘ 𝑦 ) ⟩ )
2	1	elcnvlem	⊢ ( 𝐴 ∈ ◡ ∩ { 𝑥 ∣ 𝜑 } ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 𝑦 ∈ ( V × V ) ↦ ⟨ ( 2nd ‘ 𝑦 ) , ( 1st ‘ 𝑦 ) ⟩ ) ‘ 𝐴 ) ∈ ∩ { 𝑥 ∣ 𝜑 } ) )
3	1	elcnvlem	⊢ ( 𝐴 ∈ ◡ 𝑥 ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 𝑦 ∈ ( V × V ) ↦ ⟨ ( 2nd ‘ 𝑦 ) , ( 1st ‘ 𝑦 ) ⟩ ) ‘ 𝐴 ) ∈ 𝑥 ) )
4	2 3	elmapintab	⊢ ( 𝐴 ∈ ◡ ∩ { 𝑥 ∣ 𝜑 } ↔ ( 𝐴 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ ◡ 𝑥 ) ) )