Description: Membership in a function value. (Contributed by NM, 30-Apr-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | elfv | ⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝐵 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fv2 | ⊢ ( 𝐹 ‘ 𝐵 ) = ∪ { 𝑥 ∣ ∀ 𝑦 ( 𝐵 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) } | |
2 | 1 | eleq2i | ⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) ↔ 𝐴 ∈ ∪ { 𝑥 ∣ ∀ 𝑦 ( 𝐵 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) } ) |
3 | eluniab | ⊢ ( 𝐴 ∈ ∪ { 𝑥 ∣ ∀ 𝑦 ( 𝐵 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) } ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝐵 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ) ) | |
4 | 2 3 | bitri | ⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝐵 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ) ) |