Theorem cnvintabd

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

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

Proof

Step	Hyp	Ref	Expression
1		cnvintabd.x	⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
2		pm5.5	⊢ ( ∃ 𝑥 𝜓 → ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ↔ 𝑦 ∈ ( V × V ) ) )
3	1 2	syl	⊢ ( 𝜑 → ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ↔ 𝑦 ∈ ( V × V ) ) )
4	3	bicomd	⊢ ( 𝜑 → ( 𝑦 ∈ ( V × V ) ↔ ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ) )
5	4	anbi1d	⊢ ( 𝜑 → ( ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ 𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ 𝑥 ) ) ) )
6		elcnvintab	⊢ ( 𝑦 ∈ ◡ ∩ { 𝑥 ∣ 𝜓 } ↔ ( 𝑦 ∈ ( V × V ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ 𝑥 ) ) )
7		vex	⊢ 𝑥 ∈ V
8	7	cnvex	⊢ ◡ 𝑥 ∈ V
9		relcnv	⊢ Rel ◡ 𝑥
10		df-rel	⊢ ( Rel ◡ 𝑥 ↔ ◡ 𝑥 ⊆ ( V × V ) )
11	9 10	mpbi	⊢ ◡ 𝑥 ⊆ ( V × V )
12	8 11	elmapintrab	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ 𝑥 ∧ 𝜓 ) } ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ 𝑥 ) ) ) )
13	12	elv	⊢ ( 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ 𝑥 ∧ 𝜓 ) } ↔ ( ( ∃ 𝑥 𝜓 → 𝑦 ∈ ( V × V ) ) ∧ ∀ 𝑥 ( 𝜓 → 𝑦 ∈ ◡ 𝑥 ) ) )
14	5 6 13	3bitr4g	⊢ ( 𝜑 → ( 𝑦 ∈ ◡ ∩ { 𝑥 ∣ 𝜓 } ↔ 𝑦 ∈ ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ 𝑥 ∧ 𝜓 ) } ) )
15	14	eqrdv	⊢ ( 𝜑 → ◡ ∩ { 𝑥 ∣ 𝜓 } = ∩ { 𝑤 ∈ 𝒫 ( V × V ) ∣ ∃ 𝑥 ( 𝑤 = ◡ 𝑥 ∧ 𝜓 ) } )