![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > raleqdv | GIF version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.) |
Ref | Expression |
---|---|
raleq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
raleqdv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | raleq 2555 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 = wceq 1285 ∀wral 2353 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 |
This theorem is referenced by: raleqbidv 2567 raleqbidva 2569 omsinds 4398 cbvfo 5504 isoselem 5538 ofrfval 5799 issmo2 5986 smoeq 5987 tfrlemisucaccv 6022 tfr1onlemsucaccv 6038 tfrcllemsucaccv 6051 fzrevral2 9413 fzrevral3 9414 fzshftral 9415 fzoshftral 9538 uzsinds 9737 caucvgre 10241 cvg1nlemres 10245 rexuz3 10250 resqrexlemoverl 10281 resqrexlemsqa 10284 resqrexlemex 10285 climconst 10503 climshftlemg 10515 serif0 10563 zsupcllemstep 10721 zsupcllemex 10722 infssuzex 10725 prmind2 10882 |
Copyright terms: Public domain | W3C validator |