Description: Two ways of saying a set is an element of the intersection of a class. (Contributed by RP, 13-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | elintabg | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elintg | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } 𝐴 ∈ 𝑦 ) ) | |
2 | eleq2w | ⊢ ( 𝑦 = 𝑥 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥 ) ) | |
3 | 2 | ralab2 | ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } 𝐴 ∈ 𝑦 ↔ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) |
4 | 1 3 | bitrdi | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) ) |