![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rgen2 | GIF version |
Description: Generalization rule for restricted quantification. (Contributed by NM, 30-May-1999.) |
Ref | Expression |
---|---|
rgen2.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) |
Ref | Expression |
---|---|
rgen2 | ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rgen2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) | |
2 | 1 | ralrimiva 2550 | . 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐵 𝜑) |
3 | 2 | rgen 2530 | 1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2148 ∀wral 2455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-ral 2460 |
This theorem is referenced by: rgen3 2564 f1stres 6154 f2ndres 6155 exmidonfinlem 7186 netap 7243 2onetap 7244 2omotaplemap 7246 divfnzn 9607 1arith 12345 mgmidmo 12680 isabli 12927 txuni2 13416 divcnap 13715 abscncf 13732 recncf 13733 imcncf 13734 cjcncf 13735 reefiso 13858 ioocosf1o 13935 |
Copyright terms: Public domain | W3C validator |