Theorem elcnvcnvintab

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

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

Proof

Step	Hyp	Ref	Expression
1		cnvcnv	⊢ ◡ ◡ ∩ { 𝑥 ∣ 𝜑 } = ( ∩ { 𝑥 ∣ 𝜑 } ∩ ( V × V ) )
2		incom	⊢ ( ∩ { 𝑥 ∣ 𝜑 } ∩ ( V × V ) ) = ( ( V × V ) ∩ ∩ { 𝑥 ∣ 𝜑 } )
3	1 2	eqtri	⊢ ◡ ◡ ∩ { 𝑥 ∣ 𝜑 } = ( ( V × V ) ∩ ∩ { 𝑥 ∣ 𝜑 } )
4	3	eleq2i	⊢ ( 𝐴 ∈ ◡ ◡ ∩ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ ( ( V × V ) ∩ ∩ { 𝑥 ∣ 𝜑 } ) )
5		elinintab	⊢ ( 𝐴 ∈ ( ( V × V ) ∩ ∩ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
6	4 5	bitri	⊢ ( 𝐴 ∈ ◡ ◡ ∩ { 𝑥 ∣ 𝜑 } ↔ ( 𝐴 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )