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 2624 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1331 ∀wral 2414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ral 2419 |
This theorem is referenced by: raleqbidv 2636 raleqbidva 2638 omsinds 4530 cbvfo 5679 isoselem 5714 ofrfval 5983 issmo2 6179 smoeq 6180 tfrlemisucaccv 6215 tfr1onlemsucaccv 6231 tfrcllemsucaccv 6244 fzrevral2 9879 fzrevral3 9880 fzshftral 9881 fzoshftral 10008 uzsinds 10208 iseqf1olemqk 10260 seq3f1olemstep 10267 seq3f1olemp 10268 caucvgre 10746 cvg1nlemres 10750 rexuz3 10755 resqrexlemoverl 10786 resqrexlemsqa 10789 resqrexlemex 10790 climconst 11052 climshftlemg 11064 serf0 11114 summodclem2 11144 summodc 11145 zsumdc 11146 mertenslemi1 11297 zsupcllemstep 11627 zsupcllemex 11628 infssuzex 11631 prmind2 11790 ennnfoneleminc 11913 ennnfonelemex 11916 ennnfonelemnn0 11924 ennnfonelemr 11925 lmfval 12350 lmconst 12374 cncnp 12388 metss 12652 sin0pilem2 12852 nninfsellemdc 13195 nninfself 13198 nninfsellemeqinf 13201 nninfomni 13204 |
Copyright terms: Public domain | W3C validator |