Theorem elinintrab

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

	Ref	Expression
Assertion	elinintrab	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑤 ∈ 𝒫 𝐵 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐵 ∩ 𝑥 ) ∧ 𝜑 ) } ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	inex2	⊢ ( 𝐵 ∩ 𝑥 ) ∈ V
3		inss1	⊢ ( 𝐵 ∩ 𝑥 ) ⊆ 𝐵
4	2 3	elmapintrab	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑤 ∈ 𝒫 𝐵 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐵 ∩ 𝑥 ) ∧ 𝜑 ) } ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ ( 𝐵 ∩ 𝑥 ) ) ) ) )
5		elin	⊢ ( 𝐴 ∈ ( 𝐵 ∩ 𝑥 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥 ) )
6	5	imbi2i	⊢ ( ( 𝜑 → 𝐴 ∈ ( 𝐵 ∩ 𝑥 ) ) ↔ ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥 ) ) )
7		jcab	⊢ ( ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝑥 ) ) ↔ ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
8	6 7	bitri	⊢ ( ( 𝜑 → 𝐴 ∈ ( 𝐵 ∩ 𝑥 ) ) ↔ ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
9	8	albii	⊢ ( ∀ 𝑥 ( 𝜑 → 𝐴 ∈ ( 𝐵 ∩ 𝑥 ) ) ↔ ∀ 𝑥 ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
10		19.26	⊢ ( ∀ 𝑥 ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
11		19.23v	⊢ ( ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐵 ) ↔ ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) )
12	11	anbi1i	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
13	10 12	bitri	⊢ ( ∀ 𝑥 ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
14	9 13	bitri	⊢ ( ∀ 𝑥 ( 𝜑 → 𝐴 ∈ ( 𝐵 ∩ 𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
15	14	anbi2i	⊢ ( ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ ( 𝐵 ∩ 𝑥 ) ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ) )
16		anabs5	⊢ ( ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
17	15 16	bitri	⊢ ( ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ ( 𝐵 ∩ 𝑥 ) ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
18	4 17	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑤 ∈ 𝒫 𝐵 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐵 ∩ 𝑥 ) ∧ 𝜑 ) } ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ) )