![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralbidva | GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbidva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1421 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | ralbida 2320 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 ∈ wcel 1393 ∀wral 2306 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-ral 2311 |
This theorem is referenced by: raleqbidva 2519 poinxp 4409 funimass4 5224 funimass3 5283 funconstss 5285 cocan1 5427 cocan2 5428 isocnv2 5452 isores2 5453 isoini2 5458 ofrfval 5720 ofrfval2 5727 dfsmo2 5902 smores 5907 smores2 5909 ac6sfi 6352 ordiso2 6357 caucvgsrlemcau 6877 zextlt 8332 prime 8337 fzshftral 8970 clim 9802 clim2 9804 clim2c 9805 clim0c 9807 climabs0 9828 climrecvg1n 9867 sqrt2irr 9878 |
Copyright terms: Public domain | W3C validator |