![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2ralbidv | GIF version |
Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.) |
Ref | Expression |
---|---|
2ralbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2ralbidv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | ralbidv 2477 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | ralbidv 2477 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∀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: cbvral3v 2719 poeq1 4300 soeq1 4316 isoeq1 5802 isoeq2 5803 isoeq3 5804 fnmpoovd 6216 smoeq 6291 xpf1o 6844 tapeq1 7251 elinp 7473 cauappcvgpr 7661 seq3caopr2 10482 addcn2 11318 mulcn2 11320 sgrp1 12816 ismhm 12853 issubm 12863 isnsg 13062 nmznsg 13073 iscmn 13096 ring1 13236 issubrg3 13368 islmod 13381 lmodlema 13382 ispsmet 13826 ismet 13847 isxmet 13848 addcncntoplem 14054 elcncf 14063 |
Copyright terms: Public domain | W3C validator |