Metamath Proof Explorer
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypothesis |
bnj1317.1 |
⊢ 𝐴 = { 𝑥 ∣ 𝜑 } |
|
Assertion |
bnj1317 |
⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1317.1 |
⊢ 𝐴 = { 𝑥 ∣ 𝜑 } |
2 |
|
hbab1 |
⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ∀ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) |
3 |
1 2
|
hbxfreq |
⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 ) |