Theorem cnvcnvintabd

Description: Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020)

	Ref	Expression
Hypothesis	cnvcnvintabd.x	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
Assertion	cnvcnvintabd	⊢ ( 𝜑 → ◡ ◡ ∩ { 𝑥 ∣ 𝜓 } = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } )

Proof

Step	Hyp	Ref	Expression
1		cnvcnvintabd.x	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
2		cnvcnv	⊢ ◡ ◡ 𝑥 = ( 𝑥 ∩ ( V × V ) )
3	2	eleq2i	⊢ ( 𝑦 ∈ ◡ ◡ 𝑥 ↔ 𝑦 ∈ ( 𝑥 ∩ ( V × V ) ) )
4		elin	⊢ ( 𝑦 ∈ ( 𝑥 ∩ ( V × V ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ( V × V ) ) )
5	4	rbaib	⊢ ( 𝑦 ∈ ( V × V ) → ( 𝑦 ∈ ( 𝑥 ∩ ( V × V ) ) ↔ 𝑦 ∈ 𝑥 ) )
6	3 5	bitrid	⊢ ( 𝑦 ∈ ( V × V ) → ( 𝑦 ∈ ◡ ◡ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
7	6	bicomd	⊢ ( 𝑦 ∈ ( V × V ) → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ◡ ◡ 𝑥 ) )
8	7	imbi2d	⊢ ( 𝑦 ∈ ( V × V ) → ( ( 𝜓 → 𝑦 ∈ 𝑥 ) ↔ ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) )
9	8	albidv	⊢ ( 𝑦 ∈ ( V × V ) → ( ∀ 𝑥 ( 𝜓 → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) )
10	9	pm5.32i	⊢ ( ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ 𝑥 ) ) ↔ ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) )
11		pm5.5	⊢ ( ∃ 𝑥 𝜓 → ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ↔ 𝑦 ∈ ( V × V ) ) )
12	1 11	syl	⊢ ( 𝜑 → ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ↔ 𝑦 ∈ ( V × V ) ) )
13	12	bicomd	⊢ ( 𝜑 → ( 𝑦 ∈ ( V × V ) ↔ ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ) )
14	13	anbi1d	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) ) )
15	10 14	bitrid	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ 𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) ) )
16		elcnvcnvintab	⊢ ( 𝑦 ∈ ◡ ◡ ∩ { 𝑥 ∣ 𝜓 } ↔ ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ 𝑥 ) ) )
17		vex	⊢ 𝑥 ∈ V
18		cnvexg	⊢ ( 𝑥 ∈ V → ◡ 𝑥 ∈ V )
19		cnvexg	⊢ ( ◡ 𝑥 ∈ V → ◡ ◡ 𝑥 ∈ V )
20	17 18 19	mp2b	⊢ ◡ ◡ 𝑥 ∈ V
21		relcnv	⊢ Rel ◡ ◡ 𝑥
22		df-rel	⊢ ( Rel ◡ ◡ 𝑥 ↔ ◡ ◡ 𝑥 ⊆ ( V × V ) )
23	21 22	mpbi	⊢ ◡ ◡ 𝑥 ⊆ ( V × V )
24	20 23	elmapintrab	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) ) )
25	24	elv	⊢ ( 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ ◡ 𝑥 ) ) )
26	15 16 25	3bitr4g	⊢ ( 𝜑 → ( 𝑦 ∈ ◡ ◡ ∩ { 𝑥 ∣ 𝜓 } ↔ 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } ) )
27	26	eqrdv	⊢ ( 𝜑 → ◡ ◡ ∩ { 𝑥 ∣ 𝜓 } = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ ◡ 𝑥 ∧ 𝜓 ) } )