Metamath Proof Explorer
Description: Generalization rule for restricted quantification. Note that x and
y needn't be distinct. (Contributed by NM, 18-Jun-2014)
|
|
Ref |
Expression |
|
Hypothesis |
rgenw.1 |
⊢ 𝜑 |
|
Assertion |
rgen2w |
⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
rgenw.1 |
⊢ 𝜑 |
2 |
1
|
rgenw |
⊢ ∀ 𝑦 ∈ 𝐵 𝜑 |
3 |
2
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 |