![]() |
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 2490 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | ralbidv 2490 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∀wral 2468 |
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 1458 ax-gen 1460 ax-4 1521 ax-17 1537 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 |
This theorem is referenced by: cbvral3v 2733 poeq1 4317 soeq1 4333 isoeq1 5822 isoeq2 5823 isoeq3 5824 fnmpoovd 6239 smoeq 6314 xpf1o 6871 tapeq1 7280 elinp 7502 cauappcvgpr 7690 seq3caopr2 10512 addcn2 11349 mulcn2 11351 sgrp1 12871 ismhm 12910 mhmex 12911 issubm 12921 isnsg 13138 nmznsg 13149 isghm 13179 iscmn 13229 ring1 13408 opprsubrngg 13555 issubrg3 13591 islmod 13604 lmodlema 13605 lsssetm 13669 islssmd 13672 islidlm 13792 ispsmet 14275 ismet 14296 isxmet 14297 addcncntoplem 14503 elcncf 14512 |
Copyright terms: Public domain | W3C validator |